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