functor (M : Memory.Model->
  sig
    type logic = M.loc Memory.logic
    type region = M.loc Memory.sloc list
    val value : M.loc Memory.logic -> Lang.F.term
    val loc : M.loc Memory.logic -> M.loc
    val rdescr : M.loc Memory.sloc -> Lang.F.var list * M.loc * Lang.F.pred
    val vset_of_sloc : M.loc Memory.sloc list -> Vset.vset list
    val sloc_of_vset : Vset.vset list -> M.loc Memory.sloc list
    val vset : M.loc Memory.logic -> Vset.set
    val sloc : M.loc Memory.logic -> M.loc Memory.sloc list
    val is_single : 'Memory.logic -> bool
    val map_lift :
      (Lang.F.term -> Lang.F.term) ->
      (Vset.set -> Vset.set) -> M.loc Memory.logic -> 'Memory.logic
    val apply_lift :
      (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
      (Vset.set -> Vset.set -> Vset.set) ->
      M.loc Memory.logic -> M.loc Memory.logic -> 'Memory.logic
    val map :
      (Lang.F.term -> Lang.F.term) -> M.loc Memory.logic -> 'Memory.logic
    val map_opp : M.loc Memory.logic -> 'Memory.logic
    val apply :
      (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
      M.loc Memory.logic -> M.loc Memory.logic -> 'Memory.logic
    val apply_add :
      M.loc Memory.logic -> M.loc Memory.logic -> 'Memory.logic
    val apply_sub :
      M.loc Memory.logic -> M.loc Memory.logic -> 'Memory.logic
    val map_loc : (M.loc -> 'a) -> M.loc Memory.logic -> 'Memory.logic
    val map_l2t :
      (M.loc -> Lang.F.term) -> M.loc Memory.logic -> 'Memory.logic
    val map_t2l :
      (Lang.F.term -> 'a) -> M.loc Memory.logic -> 'Memory.logic
    val field :
      M.loc Memory.logic -> Cil_types.fieldinfo -> M.loc Memory.logic
    val restrict : Vset.vset -> int option -> Vset.vset
    val shift_set :
      M.loc Memory.sloc ->
      Ctypes.c_object -> int option -> Vset.vset -> M.loc Memory.sloc
    val shift :
      M.loc Memory.logic ->
      Ctypes.c_object ->
      ?size:int -> M.loc Memory.logic -> M.loc Memory.logic
    type loader = {
      mutable sloc : M.loc Memory.sloc list;
      mutable vset : Vset.vset list;
    }
    val flush : bool -> Cvalues.Logic.loader -> M.loc Memory.logic
    val loadsloc :
      Cvalues.Logic.loader ->
      M.sigma -> Ctypes.c_object -> M.loc Memory.sloc -> unit
    val load :
      M.sigma -> Ctypes.c_object -> M.loc Memory.logic -> M.loc Memory.logic
    val union :
      Cil_types.logic_type -> M.loc Memory.logic list -> M.loc Memory.logic
    val inter :
      Cil_types.logic_type -> M.loc Memory.logic list -> 'Memory.logic
    val rloc : Ctypes.c_object -> 'Memory.sloc -> 'Memory.rloc
    val separated_sloc :
      Lang.F.pred list ->
      Ctypes.c_object * M.loc Memory.sloc list ->
      Ctypes.c_object * M.loc Memory.sloc list -> Lang.F.pred list
    val separated_from :
      Lang.F.pred list ->
      Ctypes.c_object * M.loc Memory.sloc list ->
      (Ctypes.c_object * M.loc Memory.sloc list) list -> Lang.F.pred list
    val separated_regions :
      Lang.F.pred list ->
      (Ctypes.c_object * M.loc Memory.sloc list) list -> Lang.F.pred list
    val separated :
      (Ctypes.c_object * M.loc Memory.sloc list) list -> Lang.F.pred
    val included_sloc :
      Ctypes.c_object ->
      M.loc Memory.sloc ->
      Ctypes.c_object -> M.loc Memory.sloc -> Lang.F.pred
    val included :
      Ctypes.c_object ->
      M.loc Memory.sloc list ->
      Ctypes.c_object -> M.loc Memory.sloc list -> Lang.F.pred
    val valid_sloc :
      M.sigma ->
      Memory.acs -> Ctypes.c_object -> M.loc Memory.sloc -> Lang.F.pred
    val valid :
      M.sigma ->
      Memory.acs -> Ctypes.c_object -> M.loc Memory.sloc list -> Lang.F.pred
  end