module Smart_stmt:sig
..end
val stmt : Cil_types.stmtkind -> Cil_types.stmt
Create a statement from a statement kind.
val 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 block_stmt : Cil_types.block -> Cil_types.stmt
Create a block statement from a block
val block_from_stmts : Cil_types.stmt list -> Cil_types.stmt
Create a block statement from a statement list.
val assigns : loc:Cil_types.location ->
result:Cil_types.lval -> Cil_types.exp -> Cil_types.stmt
assigns ~loc ~result value
create a statement to assign the value
expression to the result
lval.
val if_stmt : loc:Cil_types.location ->
cond:Cil_types.exp ->
?else_blk:Cil_types.block -> Cil_types.block -> Cil_types.stmt
if ~loc ~cond ~then_blk ~else_blk
create an if statement with cond
as condition and then_blk
and else_blk
as respectively "then" block and
"else" block.
val break : loc:Cil_types.location -> Cil_types.stmt
Create a break statement
val lib_call : loc:Cil_types.location ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
Construct a call to a library function with the given name.
Rtl.Symbols.Unregistered
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 rtl_call : loc:Cil_types.location ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
Special version of lib_call
for E-ACSL's RTL functions.
val 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 duplicate_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
Same as store_stmt
for __e_acsl_duplicate_store_block
that first
checks for a previous allocation of the given varinfo.
val delete_stmt : ?is_addr:bool -> Cil_types.varinfo -> Cil_types.stmt
Same as store_stmt
for __e_acsl_delete_block
that observes the
de-allocation of the given varinfo.
If is_addr
is false (default), take the address of varinfo.
val full_init_stmt : Cil_types.varinfo -> Cil_types.stmt
Same as store_stmt
for __e_acsl_full_init
that observes the
initialization of the given varinfo. The varinfo is the address to fully
initialize, no addrOf
is taken.
val initialize : loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
Same as store_stmt
for __e_acsl_initialize
that observes the
initialization of the given left-value.
val mark_readonly : Cil_types.varinfo -> Cil_types.stmt
Same as store_stmt
for __e_acsl_markreadonly
that observes the
read-onlyness of the given varinfo.
type
annotation_kind =
| |
Assertion |
| |
Precondition |
| |
Postcondition |
| |
Invariant |
| |
RTE |
val runtime_check : annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
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
.
val runtime_check_with_msg : loc:Cil_types.location ->
string ->
annotation_kind ->
Cil_types.kernel_function -> Cil_types.exp -> Cil_types.stmt
runtime_check_with_msg kind kf e msg
generates a runtime check for e
(or !e
if reverse
is true
) by building a call to __e_acsl_assert
.
msg
is the message printed if the runtime check fails. loc
is the
location printed in the message if the runtime check fails. kf
is the
current kernel_function and kind
is the annotation kind of p
.