sig
exception Unregistered_library_function of string
val get_lib_fun_vi : string -> Cil_types.varinfo
val mk_call :
loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
val mk_deref :
loc:Cil_datatype.Location.t -> Cil_types.exp -> Cil_types.exp
type annotation_kind =
Assertion
| Precondition
| Postcondition
| Invariant
| RTE
val mk_e_acsl_guard :
?reverse:bool ->
Misc.annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
val mk_block :
Project.t -> Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
val result_lhost : Cil_types.kernel_function -> Cil_types.lhost
val result_vi : Cil_types.kernel_function -> Cil_types.varinfo
val library_files : unit -> string list
val is_library_loc : Cil_types.location -> bool
val register_library_function : Cil_types.varinfo -> unit
val reset : unit -> unit
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
val term_addr_of :
loc:Cil_types.location ->
Cil_types.term_lval -> Cil_types.typ -> Cil_types.term
val reorder_ast : unit -> unit
val cty : Cil_types.logic_type -> Cil_types.typ
val ptr_index :
?loc:Cil_types.location ->
?index:Cil_types.exp -> Cil_types.exp -> Cil_types.exp * Cil_types.exp
val term_of_li : Cil_types.logic_info -> Cil_types.term
end