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

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

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