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
creates a statement to assign the value
expression to the result
lval.
val assigns_field : loc:Cil_types.location ->
Cil_types.varinfo -> string -> Cil_types.exp -> Cil_types.stmt
assigns_field ~loc vi field value
creates a statement to assign the
value
expression to the field
of the structure in the variable vi
.
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
creates 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 struct_local_init : loc:Cil_types.location ->
Cil_types.varinfo -> (string * Cil_types.exp) list -> Cil_types.stmt
struct_local_init ~loc vi fields
creates a local initialization for the
structure variable vi
. fields
is a list of couple (name, e)
where
name
is the name of a field in the structure and e
is the expression to
initialize that field.
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.