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.assigns ->
          (Ctypes.c_object * LogicSemantics.Make.region) list option
        val assigns_from :
          LogicSemantics.Make.env ->
          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