Module Constructor

module Constructor: sig .. end
Smart constructors for building C code.

Handling the E-ACSL's C-libraries, part II



val mk_deref : loc:Cil_datatype.Location.t -> Cil_types.exp -> Cil_types.exp
Construct a dereference of an expression.
val mk_block : Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
Create a block statement from a block to replace a given statement. Requires that (1) the block is not empty, or (2) the statement is a skip.
val mk_lib_call : loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
Construct a call to a library function with the given name.
Raises Unregistered_library_function if the given string does not represent such a function or if library functions were never registered (only possible when using E-ACSL through its API).
val mk_rtl_call : loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
Special version of mk_lib_call for E-ACSL's RTL functions.
val mk_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
Construct a call to __e_acsl_store_block that observes the allocation of the given varinfo. See share/e-acsl/e_acsl.h for details about this function.
val mk_duplicate_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
Same as mk_store_stmt for __e_acsl_duplicate_store_block that first checks for a previous allocation of the given varinfo.
val mk_delete_stmt : Cil_types.varinfo -> Cil_types.stmt
Same as mk_store_stmt for __e_acsl_delete_block that observes the de-allocation of the given varinfo.
val mk_full_init_stmt : ?addr:bool -> Cil_types.varinfo -> Cil_types.stmt
Same as mk_store_stmt for __e_acsl_full_init that observes the initialization of the given varinfo.
val mk_initialize : loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
Same as mk_store_stmt for __e_acsl_initialize that observes the initialization of the given left-value.
val mk_mark_readonly : Cil_types.varinfo -> Cil_types.stmt
Same as mk_store_stmt for __e_acsl_markreadonly that observes the read-onlyness of the given varinfo.
type annotation_kind = 
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
val mk_runtime_check : ?reverse:bool ->
annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
mk_runtime_check kind kf e p generates a runtime check for predicate p by building a call to __e_acsl_assert. e (or !e if reverse is set to true) is the C translation of p, kf is the current kernel_function and kind is the annotation kind of p.