Module isla_lib::memory

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

Memory

Enums

Region

Traits

MemoryCallbacks
MemoryCallbacksClone

Functions

smt_address_constraint

Type Definitions

Address

For now, we assume that we only deal with 64-bit architectures.