sig
  val new_code_annotation :
    Cil_types.code_annotation_node -> Cil_types.code_annotation
  val fresh_code_annotation : unit -> int
  val refresh_code_annotation :
    Cil_types.code_annotation -> Cil_types.code_annotation
  val refresh_spec : Cil_types.funspec -> Cil_types.funspec
  val toplevel_predicate :
    ?kind:Cil_types.predicate_kind ->
    Cil_types.predicate -> Cil_types.toplevel_predicate
  val new_predicate :
    ?kind:Cil_types.predicate_kind ->
    Cil_types.predicate -> Cil_types.identified_predicate
  val new_acsl_extension :
    string ->
    Cil_types.location ->
    bool -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension
  val refresh_predicate :
    Cil_types.identified_predicate -> Cil_types.identified_predicate
  val fresh_predicate_id : unit -> int
  val pred_of_id_pred : Cil_types.identified_predicate -> Cil_types.predicate
  val new_identified_term : Cil_types.term -> Cil_types.identified_term
  val refresh_identified_term :
    Cil_types.identified_term -> Cil_types.identified_term
  val fresh_term_id : unit -> int
  val pre_label : Cil_types.logic_label
  val post_label : Cil_types.logic_label
  val here_label : Cil_types.logic_label
  val old_label : Cil_types.logic_label
  val loop_current_label : Cil_types.logic_label
  val loop_entry_label : Cil_types.logic_label
  val init_label : Cil_types.logic_label
  val unamed :
    ?loc:Cil_types.location ->
    Cil_types.predicate_node -> Cil_types.predicate
  val ptrue : Cil_types.predicate
  val pfalse : Cil_types.predicate
  val pold :
    ?loc:Cil_types.location -> Cil_types.predicate -> Cil_types.predicate
  val papp :
    ?loc:Cil_types.location ->
    Cil_types.logic_info * Cil_types.logic_label list * Cil_types.term list ->
    Cil_types.predicate
  val pand :
    ?loc:Cil_types.location ->
    Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate
  val por :
    ?loc:Cil_types.location ->
    Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate
  val pxor :
    ?loc:Cil_types.location ->
    Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate
  val pnot :
    ?loc:Cil_types.location -> Cil_types.predicate -> Cil_types.predicate
  val pands : Cil_types.predicate list -> Cil_types.predicate
  val pors : Cil_types.predicate list -> Cil_types.predicate
  val plet :
    ?loc:Cil_types.location ->
    Cil_types.logic_info -> Cil_types.predicate -> Cil_types.predicate
  val pimplies :
    ?loc:Cil_types.location ->
    Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate
  val pif :
    ?loc:Cil_types.location ->
    Cil_types.term * Cil_types.predicate * Cil_types.predicate ->
    Cil_types.predicate
  val piff :
    ?loc:Cil_types.location ->
    Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate
  val prel :
    ?loc:Cil_types.location ->
    Cil_types.relation * Cil_types.term * Cil_types.term ->
    Cil_types.predicate
  val pforall :
    ?loc:Cil_types.location ->
    Cil_types.quantifiers * Cil_types.predicate -> Cil_types.predicate
  val pexists :
    ?loc:Cil_types.location ->
    Cil_types.quantifiers * Cil_types.predicate -> Cil_types.predicate
  val pfresh :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.logic_label * Cil_types.term *
    Cil_types.term -> Cil_types.predicate
  val pallocable :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
  val pfreeable :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
  val pvalid_read :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
  val pvalid :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
  val pobject_pointer :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
  val pvalid_function :
    ?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate
  val pinitialized :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
  val pdangling :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
  val pat :
    ?loc:Cil_types.location ->
    Cil_types.predicate * Cil_types.logic_label -> Cil_types.predicate
  val pvalid_index :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term * Cil_types.term ->
    Cil_types.predicate
  val pvalid_range :
    ?loc:Cil_types.location ->
    Cil_types.logic_label * Cil_types.term * Cil_types.term * Cil_types.term ->
    Cil_types.predicate
  val pseparated :
    ?loc:Cil_types.location -> Cil_types.term list -> Cil_types.predicate
  val instantiate :
    (string * Cil_types.logic_type) list ->
    Cil_types.logic_type -> Cil_types.logic_type
  val is_unrollable_ltdef : Cil_types.logic_type_info -> bool
  val unroll_ltdef : Cil_types.logic_type -> Cil_types.logic_type
  val isLogicCType : (Cil_types.typ -> bool) -> Cil_types.logic_type -> bool
  val is_list_type : Cil_types.logic_type -> bool
  val make_type_list_of : Cil_types.logic_type -> Cil_types.logic_type
  val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type
  val is_set_type : Cil_types.logic_type -> bool
  val set_conversion :
    Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_type
  val make_set_type : Cil_types.logic_type -> Cil_types.logic_type
  val type_of_element : Cil_types.logic_type -> Cil_types.logic_type
  val plain_or_set :
    (Cil_types.logic_type -> 'a) -> Cil_types.logic_type -> 'a
  val transform_element :
    (Cil_types.logic_type -> Cil_types.logic_type) ->
    Cil_types.logic_type -> Cil_types.logic_type
  val is_plain_type : Cil_types.logic_type -> bool
  val make_arrow_type :
    Cil_types.logic_var list -> Cil_types.logic_type -> Cil_types.logic_type
  val is_boolean_type : Cil_types.logic_type -> bool
  val boolean_type : Cil_types.logic_type
  val term :
    ?loc:Cil_datatype.Location.t ->
    Cil_types.term_node -> Cil_types.logic_type -> Cil_types.term
  val taddrof :
    ?loc:Cil_datatype.Location.t ->
    Cil_types.term_lval -> Cil_types.logic_type -> Cil_types.term
  val trange :
    ?loc:Cil_datatype.Location.t ->
    Cil_types.term option * Cil_types.term option -> Cil_types.term
  val tinteger : ?loc:Cil_datatype.Location.t -> int -> Cil_types.term
  val tinteger_s64 : ?loc:Cil_datatype.Location.t -> int64 -> Cil_types.term
  val tint : ?loc:Cil_datatype.Location.t -> Integer.t -> Cil_types.term
  val treal : ?loc:Cil_datatype.Location.t -> float -> Cil_types.term
  val treal_zero :
    ?loc:Cil_datatype.Location.t ->
    ?ltyp:Cil_types.logic_type -> unit -> Cil_types.term
  val tstring : ?loc:Cil_datatype.Location.t -> string -> Cil_types.term
  val tat :
    ?loc:Cil_datatype.Location.t ->
    Cil_types.term * Cil_types.logic_label -> Cil_types.term
  val told : ?loc:Cil_datatype.Location.t -> Cil_types.term -> Cil_types.term
  val tvar :
    ?loc:Cil_datatype.Location.t -> Cil_types.logic_var -> Cil_types.term
  val tresult :
    ?loc:Cil_datatype.Location.t -> Cil_types.typ -> Cil_types.term
  val tcast :
    ?loc:Cil_datatype.Location.t ->
    Cil_types.term -> Cil_types.typ -> Cil_types.term
  val tlogic_coerce :
    ?loc:Cil_datatype.Location.t ->
    Cil_types.term -> Cil_types.logic_type -> Cil_types.term
  val is_result : Cil_types.term -> bool
  val is_exit_status : Cil_types.term -> bool
  val lastTermOffset : Cil_types.term_offset -> Cil_types.term_offset
  val addTermOffset :
    Cil_types.term_offset -> Cil_types.term_offset -> Cil_types.term_offset
  val addTermOffsetLval :
    Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
end