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