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