Struct haybale::simple_memory::Memory
source · pub struct Memory { /* private fields */ }
Implementations§
source§impl Memory
impl Memory
pub const CELL_BITS: u32 = 8u32
pub const BITS_IN_BYTE: u32 = 8u32
pub const LOG_BITS_IN_BYTE: u32 = 3u32
pub const CELL_BYTES: u32 = 1u32
sourcepub fn new_uninitialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32
) -> Self
pub fn new_uninitialized( btor: Rc<Btor>, null_detection: bool, name: Option<&str>, addr_bits: u32 ) -> Self
A new Memory
, whose contents at all addresses are completely uninitialized (unconstrained)
null_detection
: if true
, all memory accesses will be checked to ensure
their addresses cannot be NULL, throwing Error::NullPointerDereference
if NULL is a possible solution for the address
name
: a name for this Memory
, or None
to use the default name (as of this writing, ‘mem’)
addr_bits
: e.g. 64
for a Memory
which uses 64-bit addresses
sourcepub fn new_zero_initialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32
) -> Self
pub fn new_zero_initialized( btor: Rc<Btor>, null_detection: bool, name: Option<&str>, addr_bits: u32 ) -> Self
A new Memory
, whose contents at all addresses are initialized to be 0
null_detection
: if true
, all memory accesses will be checked to ensure
their addresses cannot be NULL, throwing Error::NullPointerDereference
if NULL is a possible solution for the address
name
: a name for this Memory
, or None
to use the default name (as of this writing, ‘mem_initialized’)
addr_bits
: e.g. 64
for a Memory
which uses 64-bit addresses
sourcepub fn get_solver(&self) -> Rc<Btor>
pub fn get_solver(&self) -> Rc<Btor>
Get a reference to the Btor
instance this Memory
belongs to
sourcepub fn change_solver(&mut self, new_btor: Rc<Btor>)
pub fn change_solver(&mut self, new_btor: Rc<Btor>)
Adapt the Memory
to a new Btor
instance.
The new Btor
instance should have been created (possibly transitively)
via Btor::duplicate()
from the Btor
this Memory
was originally
created with (or most recently changed to). Further, no new variables
should have been added since the call to Btor::duplicate()
.
Trait Implementations§
source§impl Memory for Memory
impl Memory for Memory
type SolverRef = Rc<Btor>
type Index = BV<Rc<Btor>>
type Value = BV<Rc<Btor>>
source§fn new_uninitialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32
) -> Self
fn new_uninitialized( btor: Rc<Btor>, null_detection: bool, name: Option<&str>, addr_bits: u32 ) -> Self
Memory
, whose contents at all addresses are completely uninitialized (unconstrained) Read moresource§fn new_zero_initialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32
) -> Self
fn new_zero_initialized( btor: Rc<Btor>, null_detection: bool, name: Option<&str>, addr_bits: u32 ) -> Self
source§fn read(&self, index: &Self::Index, bits: u32) -> Result<Self::Value>
fn read(&self, index: &Self::Index, bits: u32) -> Result<Self::Value>
BV
will have size bits
.source§fn write(&mut self, index: &Self::Index, value: Self::Value) -> Result<()>
fn write(&mut self, index: &Self::Index, value: Self::Value) -> Result<()>
source§fn get_solver(&self) -> Rc<Btor>
fn get_solver(&self) -> Rc<Btor>
Memory
belongs to