functor (M : Memory.Model->
  sig
    type value = M.loc Wp.Memory.value
    type logic = M.loc Wp.Memory.logic
    type sigma = M.Sigma.t
    type chunk = M.Chunk.t
    type call
    type frame
    val pp_frame : Format.formatter -> Wp.LogicCompiler.Make.frame -> unit
    val frame : Cil_types.kernel_function -> Wp.LogicCompiler.Make.frame
    val call :
      Cil_types.kernel_function ->
      Wp.LogicCompiler.Make.value list -> Wp.LogicCompiler.Make.call
    val call_pre :
      Wp.LogicCompiler.Make.sigma ->
      Wp.LogicCompiler.Make.call ->
      Wp.LogicCompiler.Make.sigma -> Wp.LogicCompiler.Make.frame
    val call_post :
      Wp.LogicCompiler.Make.sigma ->
      Wp.LogicCompiler.Make.call ->
      Wp.LogicCompiler.Make.sigma Wp.Memory.sequence ->
      Wp.LogicCompiler.Make.frame
    val formal : Cil_types.varinfo -> Wp.LogicCompiler.Make.value option
    val return : unit -> Cil_types.typ
    val result : unit -> Wp.Lang.F.var
    val status : unit -> Wp.Lang.F.var
    val trigger : Wp.Definitions.trigger -> unit
    val guards : Wp.LogicCompiler.Make.frame -> Wp.Lang.F.pred list
    val mem_frame : Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
    val mem_at_frame :
      Wp.LogicCompiler.Make.frame ->
      Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
    val in_frame : Wp.LogicCompiler.Make.frame -> ('-> 'b) -> '-> 'b
    val get_frame : unit -> Wp.LogicCompiler.Make.frame
    type env
    val new_env : Cil_datatype.Logic_var.t list -> Wp.LogicCompiler.Make.env
    val move :
      Wp.LogicCompiler.Make.env ->
      Wp.LogicCompiler.Make.sigma -> Wp.LogicCompiler.Make.env
    val sigma : Wp.LogicCompiler.Make.env -> Wp.LogicCompiler.Make.sigma
    val env_at :
      Wp.LogicCompiler.Make.env ->
      Wp.Clabels.c_label -> Wp.LogicCompiler.Make.env
    val mem_at :
      Wp.LogicCompiler.Make.env ->
      Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
    val env_let :
      Wp.LogicCompiler.Make.env ->
      Cil_types.logic_var ->
      Wp.LogicCompiler.Make.logic -> Wp.LogicCompiler.Make.env
    val env_letp :
      Wp.LogicCompiler.Make.env ->
      Cil_types.logic_var -> Wp.Lang.F.pred -> Wp.LogicCompiler.Make.env
    val env_letval :
      Wp.LogicCompiler.Make.env ->
      Cil_types.logic_var ->
      Wp.LogicCompiler.Make.value -> Wp.LogicCompiler.Make.env
    val term : Wp.LogicCompiler.Make.env -> Cil_types.term -> Wp.Lang.F.term
    val pred :
      Wp.LogicCompiler.polarity ->
      Wp.LogicCompiler.Make.env -> Cil_types.predicate -> Wp.Lang.F.pred
    val logic :
      Wp.LogicCompiler.Make.env ->
      Cil_types.term -> Wp.LogicCompiler.Make.logic
    val region :
      Wp.LogicCompiler.Make.env ->
      Cil_types.term -> M.loc Wp.Memory.sloc list
    val bootstrap_term :
      (Wp.LogicCompiler.Make.env -> Cil_types.term -> Wp.Lang.F.term) -> unit
    val bootstrap_pred :
      (Wp.LogicCompiler.polarity ->
       Wp.LogicCompiler.Make.env -> Cil_types.predicate -> Wp.Lang.F.pred) ->
      unit
    val bootstrap_logic :
      (Wp.LogicCompiler.Make.env ->
       Cil_types.term -> Wp.LogicCompiler.Make.logic) ->
      unit
    val bootstrap_region :
      (Wp.LogicCompiler.Make.env ->
       Cil_types.term -> M.loc Wp.Memory.sloc list) ->
      unit
    val call_fun :
      Wp.LogicCompiler.Make.env ->
      Cil_types.logic_info ->
      (Cil_types.logic_label * Cil_types.logic_label) list ->
      Wp.Lang.F.term list -> Wp.Lang.F.term
    val call_pred :
      Wp.LogicCompiler.Make.env ->
      Cil_types.logic_info ->
      (Cil_types.logic_label * Cil_types.logic_label) list ->
      Wp.Lang.F.term list -> Wp.Lang.F.pred
    val logic_var :
      Wp.LogicCompiler.Make.env ->
      Cil_types.logic_var -> Wp.LogicCompiler.Make.logic
    val logic_info :
      Wp.LogicCompiler.Make.env ->
      Cil_types.logic_info -> Wp.Lang.F.pred option
    val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
  end