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 call : loc:Cil_types.location ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
Construct a call to a function with the given name.
Not_found
if the given string does not represent a function in the
AST, for instance if the function does not exist.val rtl_call : loc:Cil_types.location ->
?result:Cil_types.lval ->
?prefix:string -> string -> Cil_types.exp list -> Cil_types.stmt
Construct a call to a library function with the given name.
prefix
defaults to the E-ACSL RTL API prefix and can be explicitely
provided to call functions without this prefix.
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 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 |
| |
Variant |
| |
RTE |
val runtime_check : pred_kind:Cil_types.predicate_kind ->
annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
runtime_check ~pred_kind 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, kind
is the annotation kind of p
and pred_kind
indicates if the assert should be blocking or not.
val runtime_check_with_msg : loc:Cil_types.location ->
string ->
pred_kind:Cil_types.predicate_kind ->
annotation_kind ->
Cil_types.kernel_function -> Cil_types.exp -> Cil_types.stmt
runtime_check_with_msg ~loc msg ~pred_kind kind kf e
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, kind
is the annotation kind of p
and pred_kind
indicates if the assert should be blocking or not.