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
  val is_set_of_ptr_or_array : Cil_types.logic_type -> bool
  val is_range_free : Cil_types.term -> bool
  val is_bitfield_pointers : Cil_types.logic_type -> bool
  val term_has_lv_from_vi : Cil_types.term -> bool
  type pred_or_term =
      PoT_pred of Cil_types.predicate
    | PoT_term of Cil_types.term
  val mk_ptr_sizeof : Cil_types.typ -> Cil_types.location -> Cil_types.exp
  val finite_min_and_max : Ival.t -> Integer.t * Integer.t
end