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
      val add_var :
        string ->
        Cil_types.logic_var -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
      val add_type_var :
        string ->
        Cil_types.logic_type -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
      val add_logic_info :
        string ->
        Cil_types.logic_info -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
      val add_logic_label :
        string ->
        Cil_types.logic_label -> Logic_typing.Lenv.t -> Logic_typing.Lenv.t
      val find_var : string -> Logic_typing.Lenv.t -> Cil_types.logic_var
      val find_type_var :
        string -> Logic_typing.Lenv.t -> Cil_types.logic_type
      val find_logic_info :
        string -> Logic_typing.Lenv.t -> Cil_types.logic_info
      val find_logic_label :
        string -> Logic_typing.Lenv.t -> Cil_types.logic_label
    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 : ?label:string -> 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 Stdlib.ref;
    remove_logic_function : string -> unit;
    remove_logic_info : Cil_types.logic_info -> 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;
    silent : bool;
    logic_type :
      Logic_typing.typing_context ->
      Cil_types.location ->
      Logic_typing.Lenv.t -> Logic_ptree.logic_type -> Cil_types.logic_type;
    type_predicate :
      Logic_typing.typing_context ->
      Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.predicate;
    type_term :
      Logic_typing.typing_context ->
      Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.term;
    type_assigns :
      Logic_typing.typing_context ->
      accept_formal:bool ->
      Logic_typing.Lenv.t -> Logic_ptree.assigns -> Cil_types.assigns;
    error :
      ''b.
        Cil_types.location ->
        ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a;
    on_error : ''b. ('-> 'b) -> (unit -> unit) -> '-> 'b;
  }
  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 : ?label:string -> 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 Stdlib.ref
             val remove_logic_function : string -> unit
             val remove_logic_info : Cil_types.logic_info -> 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, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
             val on_error : ('-> 'b) -> (unit -> unit) -> '-> 'b
           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 :
          ?explicit:bool ->
          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
        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
  val set_extension_handler :
    is_extension:(string -> bool) ->
    typer:(string ->
           Logic_typing.typing_context ->
           Cil_types.location ->
           Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind) ->
    typer_block:(string ->
                 Logic_typing.typing_context ->
                 Filepath.position * Filepath.position ->
                 string * Logic_ptree.extended_decl list ->
                 bool * Cil_types.acsl_extension_kind) ->
    unit
  val get_typer :
    string ->
    typing_context:Logic_typing.typing_context ->
    loc:Filepath.position * Filepath.position ->
    Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind
  val get_typer_block :
    string ->
    typing_context:Logic_typing.typing_context ->
    loc:Logic_ptree.location ->
    string * Logic_ptree.extended_decl list ->
    bool * Cil_types.acsl_extension_kind
end