module Memory:sig
..end
type 'a
sequence = {
|
pre : |
|
post : |
type
acs =
| |
RW |
(* |
Read-Write Access
| *) |
| |
RD |
(* |
Read-Only Access
| *) |
type 'a
value =
| |
Val of |
| |
Loc of |
type 'a
rloc =
| |
Rloc of |
|||
| |
Rrange of |
(* |
a contiguous set of location
| *) |
type 'a
sloc =
| |
Sloc of |
|||
| |
Sarray of |
(* |
full sized range (optimized assigns)
| *) |
| |
Srange of |
|||
| |
Sdescr of |
(* |
a set of location
| *) |
type 'a
logic =
| |
Vexp of |
| |
Vloc of |
| |
Vset of |
| |
Lset of |
The memory is partitioned into chunks, sets of memory locations.
module type Chunk =sig
..end
Represent the content of the memory
module type Sigma =sig
..end
typelval =
host * offset list
type
host =
| |
Mvar of |
| |
Mmem of |
| |
Mval of |
type
offset =
| |
Mfield of |
| |
Mindex of |
type
mval =
| |
Mterm |
(* |
Not a state-related value
| *) |
| |
Maddr of |
(* |
Address of l-value
| *) |
| |
Mlval of |
(* |
Load of value at l-value in current memory-state
| *) |
| |
Mchunk of |
(* |
Memory-state with the chunk description
| *) |
type
update =
| |
Mstore of |
(* |
value
| *) |
module type Model =sig
..end