module Functions: sig
.. end
Returns true
if a function whose name is given via exp
is defined and
false
otherwise
val has_fundef : Cil_types.exp -> bool
Returns true
if a function whose name is given via exp
is defined and
false
otherwise
val check : Cil_types.kernel_function -> bool
Returns true
iff code must be generated for annotations of the given
function.
val instrument : Cil_types.kernel_function -> bool
Returns true
iff the given function must be instrumented.
RTL
Operations on function belonging to the runtime library of E-ACSL
module RTL: sig
.. end
Libc
Operations on functions belonging to standard library
module Libc: sig
.. end