sig
  val type_rel : Logic_ptree.relation -> Cil_types.relation
  val type_binop : Logic_ptree.binop -> Cil_types.binop
  val unescape : string -> string
  val wcharlist_of_string : string -> int64 list
  val is_arithmetic_type : Cil_types.logic_type -> bool
  val is_integral_type : Cil_types.logic_type -> bool
  val is_set_type : Cil_types.logic_type -> bool
  val is_array_type : Cil_types.logic_type -> bool
  val is_pointer_type : Cil_types.logic_type -> bool
  val is_list_type : Cil_types.logic_type -> bool
  val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type
  val type_of_pointed : Cil_types.logic_type -> Cil_types.logic_type
  val type_of_array_elem : Cil_types.logic_type -> Cil_types.logic_type
  val type_of_set_elem : Cil_types.logic_type -> Cil_types.logic_type
  val ctype_of_pointed : Cil_types.logic_type -> Cil_types.typ
  val ctype_of_array_elem : Cil_types.logic_type -> Cil_types.typ
  val add_offset_lval :
    Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
  val arithmetic_conversion :
    Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_type
  module Lenv : sig type t val empty : unit -> Logic_typing.Lenv.t end
  type type_namespace = Typedef | Struct | Union | Enum
  module Type_namespace :
    sig
      type t = type_namespace
      val ty : t Type.t
      val name : string
      val descr : t Descr.t
      val packed_descr : Structural_descr.pack
      val reprs : t list
      val equal : t -> t -> bool
      val compare : t -> t -> int
      val hash : t -> int
      val pretty_code : Format.formatter -> t -> unit
      val internal_pretty_code :
        Type.precedence -> Format.formatter -> t -> unit
      val pretty : Format.formatter -> t -> unit
      val varname : t -> string
      val mem_project : (Project_skeleton.t -> bool) -> t -> bool
      val copy : t -> t
    end
  type typing_context = {
    is_loop : unit -> bool;
    anonCompFieldName : string;
    conditionalConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ;
    find_macro : string -> Logic_ptree.lexpr;
    find_var : string -> Cil_types.logic_var;
    find_enum_tag : string -> Cil_types.exp * Cil_types.typ;
    find_comp_field : Cil_types.compinfo -> string -> Cil_types.offset;
    find_type : Logic_typing.type_namespace -> string -> Cil_types.typ;
    find_label : string -> Cil_types.stmt Pervasives.ref;
    remove_logic_function : string -> unit;
    remove_logic_type : string -> unit;
    remove_logic_ctor : string -> unit;
    add_logic_function : Cil_types.logic_info -> unit;
    add_logic_type : string -> Cil_types.logic_type_info -> unit;
    add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit;
    find_all_logic_functions : string -> Cil_types.logic_info list;
    find_logic_type : string -> Cil_types.logic_type_info;
    find_logic_ctor : string -> Cil_types.logic_ctor_info;
    pre_state : Logic_typing.Lenv.t;
    post_state : Cil_types.termination_kind list -> Logic_typing.Lenv.t;
    assigns_env : Logic_typing.Lenv.t;
    type_predicate :
      Logic_typing.Lenv.t ->
      Logic_ptree.lexpr -> Cil_types.predicate Cil_types.named;
    type_term : Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.term;
    type_assigns :
      accept_formal:bool ->
      Logic_typing.Lenv.t ->
      Logic_ptree.lexpr Cil_types.assigns ->
      Cil_types.identified_term Cil_types.assigns;
    error :
      'a.
        Cil_types.location ->
        ('a, Format.formatter, unit) Pervasives.format -> 'a;
  }
  val register_behavior_extension :
    string ->
    (typing_context:Logic_typing.typing_context ->
     loc:Cil_types.location ->
     Cil_types.funbehavior -> Logic_ptree.lexpr list -> unit) ->
    unit
  module Make :
    functor
      (C : sig
             val is_loop : unit -> bool
             val anonCompFieldName : string
             val conditionalConversion :
               Cil_types.typ -> Cil_types.typ -> Cil_types.typ
             val find_macro : string -> Logic_ptree.lexpr
             val find_var : string -> Cil_types.logic_var
             val find_enum_tag : string -> Cil_types.exp * Cil_types.typ
             val find_type :
               Logic_typing.type_namespace -> string -> Cil_types.typ
             val find_comp_field :
               Cil_types.compinfo -> string -> Cil_types.offset
             val find_label : string -> Cil_types.stmt Pervasives.ref
             val remove_logic_function : string -> unit
             val remove_logic_type : string -> unit
             val remove_logic_ctor : string -> unit
             val add_logic_function : Cil_types.logic_info -> unit
             val add_logic_type : string -> Cil_types.logic_type_info -> unit
             val add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit
             val find_all_logic_functions :
               string -> Cil_types.logic_info list
             val find_logic_type : string -> Cil_types.logic_type_info
             val find_logic_ctor : string -> Cil_types.logic_ctor_info
             val integral_cast :
               Cil_types.typ -> Cil_types.term -> Cil_types.term
             val error :
               Cil_types.location ->
               ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
           end->
      sig
        val type_of_field :
          Cil_types.location ->
          string ->
          Cil_types.logic_type ->
          Cil_types.term_offset * Cil_types.logic_type
        val mk_cast :
          Cil_types.term -> Cil_types.logic_type -> Cil_types.term
        val term : Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.term
        val predicate :
          Logic_typing.Lenv.t ->
          Logic_ptree.lexpr -> Cil_types.predicate Cil_types.named
        val code_annot :
          Cil_types.location ->
          string list ->
          Cil_types.logic_type ->
          Logic_ptree.code_annot -> Cil_types.code_annotation
        val type_annot :
          Cil_types.location ->
          Logic_ptree.type_annot -> Cil_types.logic_info
        val model_annot :
          Cil_types.location ->
          Logic_ptree.model_annot -> Cil_types.model_info
        val annot : Logic_ptree.decl -> Cil_types.global_annotation
        val custom : Logic_ptree.custom_tree -> Cil_types.custom_tree
        val funspec :
          string list ->
          Cil_types.varinfo ->
          Cil_types.varinfo list option ->
          Cil_types.typ -> Logic_ptree.spec -> Cil_types.funspec
      end
  val append_old_and_post_labels : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
  val append_here_label : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
  val append_pre_label : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
  val append_init_label : Logic_typing.Lenv.t -> Logic_typing.Lenv.t
  val add_var :
    string ->
    Cil_types.logic_var -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
  val add_result :
    Logic_typing.Lenv.t -> Cil_types.logic_type -> Logic_typing.Lenv.t
  val enter_post_state :
    Logic_typing.Lenv.t -> Cil_types.termination_kind -> Logic_typing.Lenv.t
  val post_state_env :
    Cil_types.termination_kind -> Cil_types.logic_type -> Logic_typing.Lenv.t
end