Module Wp.Memory

module Memory: sig .. end

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

Memory Variables

The memory is partitioned into chunks, sets of memory locations.

module type Chunk = sig .. end

Memory Environment

Represent the content of the memory

module type Sigma = sig .. end

State Pretty-Printer
type lval = host * offset list 
type host = 
| Mvar of Cil_types.varinfo
| Mmem of Wp.Lang.F.term
| Mval of lval
type offset = 
| Mfield of Cil_types.fieldinfo
| Mindex of Wp.Lang.F.term
type mval = 
| Mterm (*
Not a state-related value
*)
| Maddr of lval (*
Address of l-value
*)
| Mlval of lval (*
Load of value at l-value in current memory-state
*)
| Mchunk of string (*
Memory-state with the chunk description
*)
type update = 
| Mstore of lval * Wp.Lang.F.term (*
value
*)

Memory Model
module type Model = sig .. end