sig   type polarity = [ `Negative | `NoPolarity | `Positive ]   module Make :     functor (M : Memory.Model->       sig         type loc = M.loc         type sigma = M.Sigma.t         type value = M.loc Wp.Memory.value         type logic = M.loc Wp.Memory.logic         type region = M.loc Wp.Memory.sloc list         val pp_logic :           Format.formatter -> Wp.LogicSemantics.Make.logic -> unit         val pp_sloc :           Format.formatter ->           Wp.LogicSemantics.Make.loc Wp.Memory.sloc -> unit         val pp_region :           Format.formatter -> Wp.LogicSemantics.Make.region -> unit         type call         type frame         val pp_frame :           Format.formatter -> Wp.LogicSemantics.Make.frame -> unit         val get_frame : unit -> Wp.LogicSemantics.Make.frame         val in_frame : Wp.LogicSemantics.Make.frame -> ('-> 'b) -> '-> 'b         val mem_frame : Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma         val mem_at_frame :           Wp.LogicSemantics.Make.frame ->           Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma         val call :           Cil_types.kernel_function ->           Wp.LogicSemantics.Make.value list -> Wp.LogicSemantics.Make.call         val frame : Cil_types.kernel_function -> Wp.LogicSemantics.Make.frame         val call_pre :           Wp.LogicSemantics.Make.sigma ->           Wp.LogicSemantics.Make.call ->           Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.frame         val call_post :           Wp.LogicSemantics.Make.sigma ->           Wp.LogicSemantics.Make.call ->           Wp.LogicSemantics.Make.sigma Wp.Memory.sequence ->           Wp.LogicSemantics.Make.frame         val return : unit -> Cil_types.typ         val result : unit -> Wp.Lang.F.var         val status : unit -> Wp.Lang.F.var         val guards : Wp.LogicSemantics.Make.frame -> Wp.Lang.F.pred list         type env         val new_env : Cil_types.logic_var list -> Wp.LogicSemantics.Make.env         val move :           Wp.LogicSemantics.Make.env ->           Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.env         val sigma :           Wp.LogicSemantics.Make.env -> Wp.LogicSemantics.Make.sigma         val mem_at :           Wp.LogicSemantics.Make.env ->           Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma         val call_env :           Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.env         val term :           Wp.LogicSemantics.Make.env -> Cil_types.term -> Wp.Lang.F.term         val pred :           Wp.LogicSemantics.polarity ->           Wp.LogicSemantics.Make.env -> Cil_types.predicate -> Wp.Lang.F.pred         val region :           Wp.LogicSemantics.Make.env ->           Cil_types.term -> Wp.LogicSemantics.Make.region         val assigns :           Wp.LogicSemantics.Make.env ->           Cil_types.identified_term Cil_types.assigns ->           (Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list option         val assigns_from :           Wp.LogicSemantics.Make.env ->           Cil_types.identified_term Cil_types.from list ->           (Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list         val val_of_term :           Wp.LogicSemantics.Make.env -> Cil_types.term -> Wp.Lang.F.term         val loc_of_term :           Wp.LogicSemantics.Make.env ->           Cil_types.term -> Wp.LogicSemantics.Make.loc         val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma         val vars : Wp.LogicSemantics.Make.region -> Wp.Lang.F.Vars.t         val occurs : Wp.Lang.F.var -> Wp.LogicSemantics.Make.region -> bool         val valid :           Wp.LogicSemantics.Make.sigma ->           Wp.Memory.acs ->           Wp.Ctypes.c_object ->           Wp.LogicSemantics.Make.region -> Wp.Lang.F.pred         val included :           Wp.Ctypes.c_object ->           Wp.LogicSemantics.Make.region ->           Wp.Ctypes.c_object ->           Wp.LogicSemantics.Make.region -> Wp.Lang.F.pred         val separated :           (Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list ->           Wp.Lang.F.pred       end end