Module Memory

module Memory: sig .. end
Memory Values

type 'a sequence = {
   pre : 'a;
   post : 'a;
}
Memory Values
type acs = 
| RW (*Read-Write Access*)
| RD (*Read-Only Access*)
type 'a value = 
| Val of Lang.F.term
| Loc of 'a
type 'a rloc = 
| Rloc of Ctypes.c_object * 'a
| Rarray of 'a * Ctypes.c_object * int
| Rrange of 'a * Ctypes.c_object * Lang.F.term option * Lang.F.term option
type 'a sloc = 
| Sloc of 'a
| Sarray of 'a * Ctypes.c_object * int (*full sized-array range*)
| Srange of 'a * Ctypes.c_object * Lang.F.term option * Lang.F.term option
| Sdescr of Lang.F.var list * 'a * Lang.F.pred
type 'a logic = 
| Vexp of Lang.F.term
| Vloc of 'a
| Vset of Vset.set
| Lset of 'a sloc list

Memory Variables
module type Chunk = sig .. end

Memory Environment
module type Sigma = sig .. end

Memory Model
module type Model = sig .. end