Module Functions

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