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