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