sig
val stmt : Cil_types.stmtkind -> Cil_types.stmt
val block : Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
val block_stmt : Cil_types.block -> Cil_types.stmt
val block_from_stmts : Cil_types.stmt list -> Cil_types.stmt
val assigns :
loc:Cil_types.location ->
result:Cil_types.lval -> Cil_types.exp -> Cil_types.stmt
val if_stmt :
loc:Cil_types.location ->
cond:Cil_types.exp ->
?else_blk:Cil_types.block -> Cil_types.block -> Cil_types.stmt
val break : loc:Cil_types.location -> Cil_types.stmt
val lib_call :
loc:Cil_types.location ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
val rtl_call :
loc:Cil_types.location ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
val store_stmt :
?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val duplicate_store_stmt :
?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val delete_stmt : ?is_addr:bool -> Cil_types.varinfo -> Cil_types.stmt
val full_init_stmt : Cil_types.varinfo -> Cil_types.stmt
val initialize : loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
val mark_readonly : Cil_types.varinfo -> Cil_types.stmt
type annotation_kind =
Assertion
| Precondition
| Postcondition
| Invariant
| RTE
val runtime_check :
Smart_stmt.annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
val runtime_check_with_msg :
loc:Cil_types.location ->
string ->
Smart_stmt.annotation_kind ->
Cil_types.kernel_function -> Cil_types.exp -> Cil_types.stmt
end