Expand description
The memory is split up into various regions defined by a half-open range between two addresses [base, top). This is done because we want to give different semantics to various parts of memory, e.g. program memory should be concrete, whereas the memory used for loads and stores in litmus tests need to be totally symbolic so the bevhaior can be imposed later as part of the concurrency model.
Structs§
Enums§
Traits§
Functions§
Type Aliases§
- Address
- For now, we assume that we only deal with 64-bit architectures.