functor (M : Memory.Model->
  sig
    type logic = M.loc Memory.logic
    val value : Cvalues.Logic.logic -> Lang.F.term
    val loc : Cvalues.Logic.logic -> M.loc
    val vset : Cvalues.Logic.logic -> Vset.set
    val sloc : Cvalues.Logic.logic -> M.loc Memory.sloc list
    val rdescr : M.loc Memory.sloc -> Lang.F.var list * M.loc * Lang.F.pred
    val map : Lang.F.unop -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val map_opp : Cvalues.Logic.logic -> Cvalues.Logic.logic
    val map_loc :
      (M.loc -> M.loc) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val map_l2t :
      (M.loc -> Lang.F.term) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val map_t2l :
      (Lang.F.term -> M.loc) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val apply :
      Lang.F.binop ->
      Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val apply_add :
      Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val apply_sub :
      Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val field :
      Cvalues.Logic.logic -> Cil_types.fieldinfo -> Cvalues.Logic.logic
    val shift :
      Cvalues.Logic.logic ->
      Ctypes.c_object ->
      ?size:int -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val load :
      M.Sigma.t ->
      Ctypes.c_object -> Cvalues.Logic.logic -> Cvalues.Logic.logic
    val union :
      Cil_types.logic_type -> Cvalues.Logic.logic list -> Cvalues.Logic.logic
    val inter :
      Cil_types.logic_type -> Cvalues.Logic.logic list -> Cvalues.Logic.logic
    val subset :
      Cil_types.logic_type ->
      Cvalues.Logic.logic ->
      Cil_types.logic_type -> Cvalues.Logic.logic -> Lang.F.pred
    type region = M.loc Memory.sloc list
    val separated :
      (Ctypes.c_object * Cvalues.Logic.region) list -> Lang.F.pred
    val included :
      Ctypes.c_object ->
      Cvalues.Logic.region ->
      Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred
    val valid :
      M.Sigma.t ->
      Memory.acs -> Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred
  end