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;     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 :       ''b.         Cil_types.location ->         ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a;   }   val register_behavior_extension :     string ->     (typing_context:Logic_typing.typing_context ->      loc:Cil_types.location ->      Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) ->     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         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