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 Cil_types.named -> 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