functor (M : Memory.Model->
  sig
    type value = M.loc Memory.value
    type logic = M.loc Memory.logic
    type sigma = M.Sigma.t
    type chunk = M.Chunk.t
    type signature =
        CST of Integer.t
      | SIG of LogicCompiler.Make.sig_param list
    and sig_param =
        Sig_value of Cil_types.logic_var
      | Sig_chunk of LogicCompiler.Make.chunk * Clabels.c_label
    val wrap_lvar :
      Cil_datatype.Logic_var.Map.key list ->
      'a list -> 'Cil_datatype.Logic_var.Map.t
    val wrap_var :
      Cil_datatype.Varinfo.Map.key list ->
      'a list -> 'Cil_datatype.Varinfo.Map.t
    val wrap_mem : (Clabels.LabelMap.key * 'a) list -> 'Clabels.LabelMap.t
    val fresh_lvar : ?basename:string -> Cil_types.logic_type -> Lang.F.var
    val fresh_cvar : ?basename:string -> Cil_types.typ -> Lang.F.var
    type frame = {
      name : string;
      pool : Lang.F.pool;
      gamma : Lang.gamma;
      kf : Cil_types.kernel_function option;
      formals : LogicCompiler.Make.value Cil_datatype.Varinfo.Map.t;
      types : string list;
      mutable triggers : Definitions.trigger list;
      mutable labels : LogicCompiler.Make.sigma Clabels.LabelMap.t;
      mutable result : Lang.F.var option;
      mutable status : Lang.F.var option;
    }
    val pp_frame : Format.formatter -> LogicCompiler.Make.frame -> unit
    val logic_frame : string -> string list -> LogicCompiler.Make.frame
    val frame : Kernel_function.t -> LogicCompiler.Make.frame
    val call_pre :
      Kernel_function.t ->
      LogicCompiler.Make.value list ->
      LogicCompiler.Make.sigma -> LogicCompiler.Make.frame
    val call_post :
      Kernel_function.t ->
      LogicCompiler.Make.value list ->
      LogicCompiler.Make.sigma Memory.sequence -> LogicCompiler.Make.frame
    val frame_copy : LogicCompiler.Make.frame -> LogicCompiler.Make.frame
    val cframe : LogicCompiler.Make.frame Context.value
    val get_frame : unit -> LogicCompiler.Make.frame
    val in_frame : LogicCompiler.Make.frame -> ('-> 'b) -> '-> 'b
    val mem_at_frame :
      LogicCompiler.Make.frame ->
      Clabels.LabelMap.key -> LogicCompiler.Make.sigma
    val mem_frame : Clabels.LabelMap.key -> LogicCompiler.Make.sigma
    val formal :
      Cil_datatype.Varinfo.Map.key -> LogicCompiler.Make.value option
    val return : unit -> Cil_types.typ
    val result : unit -> Lang.F.var
    val status : unit -> Lang.F.var
    val trigger : Definitions.trigger -> unit
    val guards : LogicCompiler.Make.frame -> Lang.F.pred list
    type env = {
      vars : LogicCompiler.Make.logic Cil_datatype.Logic_var.Map.t;
      lhere : LogicCompiler.Make.sigma option;
      current : LogicCompiler.Make.sigma option;
    }
    val plain_of_exp : Cil_types.logic_type -> Lang.F.term -> 'Memory.logic
    val new_env :
      Cil_datatype.Logic_var.Map.key list -> LogicCompiler.Make.env
    val sigma : LogicCompiler.Make.env -> LogicCompiler.Make.sigma
    val move :
      LogicCompiler.Make.env ->
      LogicCompiler.Make.sigma -> LogicCompiler.Make.env
    val env_at :
      LogicCompiler.Make.env ->
      Clabels.LabelMap.key -> LogicCompiler.Make.env
    val mem_at :
      LogicCompiler.Make.env ->
      Clabels.LabelMap.key -> LogicCompiler.Make.sigma
    val env_let :
      LogicCompiler.Make.env ->
      Cil_datatype.Logic_var.Map.key ->
      LogicCompiler.Make.logic -> LogicCompiler.Make.env
    val env_letval :
      LogicCompiler.Make.env ->
      Cil_datatype.Logic_var.Map.key ->
      M.loc Memory.value -> LogicCompiler.Make.env
    val param_of_lv : Cil_types.logic_var -> Lang.F.var
    val profile_env :
      LogicCompiler.Make.logic Cil_datatype.Logic_var.Map.t ->
      (Cil_datatype.Logic_var.Map.key * Lang.F.var) list ->
      Cil_datatype.Logic_var.Map.key list ->
      LogicCompiler.Make.env *
      (Cil_datatype.Logic_var.Map.key * Lang.F.var) list
    val default_label :
      LogicCompiler.Make.env ->
      Cil_types.logic_label list -> LogicCompiler.Make.env
    val compile_step :
      string ->
      string list ->
      Cil_types.logic_var list ->
      Cil_types.logic_label list ->
      (LogicCompiler.Make.env -> '-> 'b) ->
      ('-> Lang.F.var -> bool) ->
      '->
      Lang.F.var list * Definitions.trigger list * 'b *
      LogicCompiler.Make.sig_param list
    val cc_term :
      (LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term)
      Pervasives.ref
    val cc_pred :
      (bool ->
       LogicCompiler.Make.env ->
       Cil_types.predicate Cil_types.named -> Lang.F.pred)
      Pervasives.ref
    val cc_logic :
      (LogicCompiler.Make.env -> Cil_types.term -> LogicCompiler.Make.logic)
      Pervasives.ref
    val cc_region :
      (LogicCompiler.Make.env -> Cil_types.term -> M.loc Memory.sloc list)
      Pervasives.ref
    val term : LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term
    val pred :
      bool ->
      LogicCompiler.Make.env ->
      Cil_types.predicate Cil_types.named -> Lang.F.pred
    val logic :
      LogicCompiler.Make.env -> Cil_types.term -> LogicCompiler.Make.logic
    val region :
      LogicCompiler.Make.env -> Cil_types.term -> M.loc Memory.sloc list
    val reads :
      LogicCompiler.Make.env -> Cil_types.identified_term list -> unit
    val bootstrap_term :
      (LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term) -> unit
    val bootstrap_pred :
      (bool ->
       LogicCompiler.Make.env ->
       Cil_types.predicate Cil_types.named -> Lang.F.pred) ->
      unit
    val bootstrap_logic :
      (LogicCompiler.Make.env -> Cil_types.term -> LogicCompiler.Make.logic) ->
      unit
    val bootstrap_region :
      (LogicCompiler.Make.env -> Cil_types.term -> M.loc Memory.sloc list) ->
      unit
    val in_term : Lang.F.term -> Lang.F.var -> bool
    val in_pred : Lang.F.pred -> Lang.F.var -> bool
    val in_reads : '-> '-> bool
    val is_recursive : Cil_types.logic_info -> Definitions.recursion
    module Axiomatic :
      sig
        module E :
          sig
            type key = string
            type data = unit
            val name : string
            val compare : key -> key -> int
            val pretty : Format.formatter -> key -> unit
          end
        type key = E.key
        type data = E.data
        val mem : key -> bool
        val find : key -> data
        val get : key -> data option
        val define : key -> data -> unit
        val update : key -> data -> unit
        val memoize : (key -> data) -> key -> data
        val compile : (key -> data) -> key -> unit
        val callback : (key -> data -> unit) -> unit
        val iter : (key -> data -> unit) -> unit
        val iter_sorted : (key -> data -> unit) -> unit
      end
    module Signature :
      sig
        module E :
          sig
            type key = Cil_types.logic_info
            type data = signature
            val name : string
            val compare : key -> key -> int
            val pretty : Format.formatter -> key -> unit
          end
        type key = E.key
        type data = E.data
        val mem : key -> bool
        val find : key -> data
        val get : key -> data option
        val define : key -> data -> unit
        val update : key -> data -> unit
        val memoize : (key -> data) -> key -> data
        val compile : (key -> data) -> key -> unit
        val callback : (key -> data -> unit) -> unit
        val iter : (key -> data -> unit) -> unit
        val iter_sorted : (key -> data -> unit) -> unit
      end
    val compile_lemma :
      Definitions.cluster ->
      string ->
      assumed:bool ->
      string list ->
      Cil_types.logic_label list ->
      Cil_types.predicate Cil_types.named -> Definitions.dlemma
    val type_for_signature :
      Cil_types.logic_info ->
      Definitions.dfun -> LogicCompiler.Make.sig_param list -> unit
    val compile_lbpure :
      Definitions.cluster ->
      LogicCompiler.Make.Signature.key ->
      Lang.F.var list * LogicCompiler.Make.sig_param list
    val compile_lbnone :
      Definitions.cluster ->
      Cil_types.logic_info ->
      Cil_types.varinfo list -> LogicCompiler.Make.signature
    val compile_lbreads :
      Definitions.cluster ->
      Cil_types.logic_info ->
      Cil_types.identified_term list -> LogicCompiler.Make.signature
    val compile_rec :
      string ->
      LogicCompiler.Make.Signature.key ->
      (LogicCompiler.Make.env -> '-> 'b) ->
      ('-> Lang.F.var -> bool) ->
      '->
      Lang.F.var list * Definitions.trigger list * 'b *
      LogicCompiler.Make.sig_param list
    val compile_lbterm :
      Definitions.cluster ->
      LogicCompiler.Make.Signature.key ->
      Cil_types.term -> LogicCompiler.Make.signature
    val compile_lbpred :
      Definitions.cluster ->
      LogicCompiler.Make.Signature.key ->
      Cil_types.predicate Cil_types.named -> LogicCompiler.Make.signature
    val heap_case :
      Clabels.LabelSet.t Clabels.LabelMap.t ->
      Clabels.LabelSet.t M.Heap.Map.t ->
      LogicCompiler.Make.sig_param -> Clabels.LabelSet.t M.Heap.Map.t
    val compile_lbinduction :
      Definitions.cluster ->
      LogicCompiler.Make.Signature.key ->
      (string * Cil_types.logic_label list * string list *
       Cil_types.predicate Cil_types.named)
      list -> LogicCompiler.Make.signature
    val compile_logic :
      Definitions.cluster ->
      LogicUsage.logic_section ->
      LogicCompiler.Make.Signature.key -> LogicCompiler.Make.signature
    val define_type :
      Definitions.cluster -> Cil_types.logic_type_info -> unit
    val define_logic :
      Definitions.cluster ->
      LogicUsage.logic_section -> LogicCompiler.Make.Signature.key -> unit
    val define_lemma : Definitions.cluster -> LogicUsage.logic_lemma -> unit
    val define_axiomatic :
      Definitions.cluster -> LogicUsage.axiomatic -> unit
    val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
    val signature :
      LogicCompiler.Make.Signature.key -> LogicCompiler.Make.Signature.data
    val bind_labels :
      LogicCompiler.Make.env ->
      (Cil_types.logic_label * Cil_types.logic_label) list ->
      LogicCompiler.Make.sigma Clabels.LabelMap.t
    val call_params :
      LogicCompiler.Make.env ->
      Cil_types.logic_info ->
      (Cil_types.logic_label * Cil_types.logic_label) list ->
      LogicCompiler.Make.sig_param list ->
      Lang.F.term list -> Lang.F.term list
    val call_fun :
      LogicCompiler.Make.env ->
      Cil_types.logic_info ->
      (Cil_types.logic_label * Cil_types.logic_label) list ->
      Lang.F.term list -> Lang.F.term
    val call_pred :
      LogicCompiler.Make.env ->
      Cil_types.logic_info ->
      (Cil_types.logic_label * Cil_types.logic_label) list ->
      Lang.F.term list -> Lang.F.pred
    val logic_var :
      LogicCompiler.Make.env ->
      Cil_datatype.Logic_var.Map.key -> LogicCompiler.Make.logic
  end