sig
val mk_deref :
loc:Cil_datatype.Location.t -> Cil_types.exp -> Cil_types.exp
val mk_block : Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
val mk_lib_call :
loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
val mk_rtl_call :
loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
val mk_store_stmt :
?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val mk_duplicate_store_stmt :
?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val mk_delete_stmt : Cil_types.varinfo -> Cil_types.stmt
val mk_full_init_stmt : ?addr:bool -> Cil_types.varinfo -> Cil_types.stmt
val mk_initialize :
loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
val mk_mark_readonly : Cil_types.varinfo -> Cil_types.stmt
type annotation_kind =
Assertion
| Precondition
| Postcondition
| Invariant
| RTE
val mk_runtime_check :
?reverse:bool ->
Constructor.annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
end