Module Smart_stmt

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.

Raises 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.