module Constructor:sig
..end
val mk_deref : loc:Cil_datatype.Location.t -> Cil_types.exp -> Cil_types.exp
val mk_block : Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
val mk_lib_call : loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
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
mk_lib_call
for E-ACSL's RTL functions.val mk_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
__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
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
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
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
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
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
.