Module Functions

module Functions: sig .. end

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

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

Operations concerning the support of concurrency

module Concurrency: sig .. end