E_ACSL.Smart_stmt
Create a statement from a statement kind.
val block :
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.block ->
Frama_c_kernel.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 :
Frama_c_kernel.Cil_types.block ->
Frama_c_kernel.Cil_types.stmt
Create a block statement from a block
val block_from_stmts :
Frama_c_kernel.Cil_types.stmt list ->
Frama_c_kernel.Cil_types.stmt
Create a block statement from a statement list.
val assigns :
loc:Frama_c_kernel.Cil_types.location ->
result:Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.stmt
assigns ~loc ~result value
creates a statement to assign the value
expression to the result
lval.
val assigns_field :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.varinfo ->
string ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.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:Frama_c_kernel.Cil_types.location ->
cond:Frama_c_kernel.Cil_types.exp ->
?else_blk:Frama_c_kernel.Cil_types.block ->
Frama_c_kernel.Cil_types.block ->
Frama_c_kernel.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:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.stmt
Create a break statement
val struct_local_init :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.varinfo ->
(string * Frama_c_kernel.Cil_types.exp) list ->
Frama_c_kernel.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:Frama_c_kernel.Cil_types.location ->
?result:Frama_c_kernel.Cil_types.lval ->
string ->
Frama_c_kernel.Cil_types.exp list ->
Frama_c_kernel.Cil_types.stmt
Construct a call to a function with the given name.
val rtl_call :
loc:Frama_c_kernel.Cil_types.location ->
?result:Frama_c_kernel.Cil_types.lval ->
?prefix:string ->
string ->
Frama_c_kernel.Cil_types.exp list ->
Frama_c_kernel.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.
val store_stmt :
?str_size:Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.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:Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.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 ->
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.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 :
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.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:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.lval ->
Frama_c_kernel.Cil_types.stmt
Same as store_stmt
for __e_acsl_initialize
that observes the initialization of the given left-value.
val mark_readonly :
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.Cil_types.stmt
Same as store_stmt
for __e_acsl_markreadonly
that observes the read-onlyness of the given varinfo.