sig   type polarity = [ `Negative | `NoPolarity | `Positive ]   module Make :     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 end