sig
  val string_of_typ : Cil_types.typ -> string
  val ttype_of_pointed : Cil_types.logic_type -> Cil_types.logic_type
  val ptr_of : Cil_types.typ -> Cil_types.typ
  val const_of : Cil_types.typ -> Cil_types.typ
  val size_t : unit -> Cil_types.typ
  val prepare_definition : string -> Cil_types.typ -> Cil_types.fundec
  val call_function :
    Cil_types.lval option ->
    Cil_types.varinfo -> Cil_types.exp list -> Cil_types.instr
  val cvar_to_tvar : Cil_types.varinfo -> Cil_types.term
  val tunref_range :
    ?loc:Cil_types.location ->
    Cil_types.term -> Cil_types.term -> Cil_types.term
  val tunref_range_bytes_len :
    ?loc:Cil_types.location ->
    Cil_types.term -> Cil_types.term -> Cil_types.term
  val tplus :
    ?loc:Cil_types.location ->
    Cil_types.term -> Cil_types.term -> Cil_types.term
  val tminus :
    ?loc:Cil_types.location ->
    Cil_types.term -> Cil_types.term -> Cil_types.term
  val tdivide :
    ?loc:Cil_types.location ->
    Cil_types.term -> Cil_types.term -> Cil_types.term
  val pbounds_incl_excl :
    ?loc:Cil_types.location ->
    Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
  val plet_len_div_size :
    ?loc:Cil_types.location ->
    ?name_ext:string ->
    Cil_types.logic_type ->
    Cil_types.term ->
    (Cil_types.term -> Cil_types.predicate) -> Cil_types.predicate
  val punfold_all_elems_eq :
    ?loc:Cil_types.location ->
    Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
  val punfold_all_elems_pred :
    ?loc:Cil_types.location ->
    Cil_types.term ->
    Cil_types.term ->
    (?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate) ->
    Cil_types.predicate
  val punfold_flexible_struct_pred :
    ?loc:Cil_types.location ->
    Cil_types.term ->
    Cil_types.term ->
    (?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate) ->
    Cil_types.predicate
  val pvalid_len_bytes :
    ?loc:Cil_types.location ->
    Cil_types.logic_label ->
    Cil_types.term -> Cil_types.term -> Cil_types.predicate
  val pvalid_read_len_bytes :
    ?loc:Cil_types.location ->
    Cil_types.logic_label ->
    Cil_types.term -> Cil_types.term -> Cil_types.predicate
  val pcorrect_len_bytes :
    ?loc:Cil_types.location ->
    Cil_types.logic_type -> Cil_types.term -> Cil_types.predicate
  val pseparated_memories :
    ?loc:Cil_types.location ->
    Cil_types.term ->
    Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
  val make_behavior :
    ?name:string ->
    ?assumes:Cil_types.identified_predicate list ->
    ?requires:Cil_types.identified_predicate list ->
    ?ensures:(Cil_types.termination_kind * Cil_types.identified_predicate)
             list ->
    ?assigns:Cil_types.assigns ->
    ?alloc:Cil_types.allocation ->
    ?extension:Cil_types.acsl_extension list -> unit -> Cil_types.behavior
  val make_funspec :
    Cil_types.behavior list ->
    ?termination:Cil_types.identified_predicate option ->
    ?complete_disjoint:string list list * string list list ->
    unit -> Cil_types.funspec
end