Trait haybale::backend::Memory[−][src]

pub trait Memory: Clone + PartialEq + Eq {
    type SolverRef: SolverRef<BV = Self::Index>;
    type Index: BV<SolverRef = Self::SolverRef>;
    type Value: BV;
    fn new_uninitialized(
        solver: Self::SolverRef, 
        null_detection: bool, 
        name: Option<&str>, 
        addr_bits: u32
    ) -> Self;

    fn new_zero_initialized(
        solver: Self::SolverRef, 
        null_detection: bool, 
        name: Option<&str>, 
        addr_bits: u32
    ) -> Self;

    fn read(&self, index: &Self::Index, bits: u32) -> Result<Self::Value>;

    fn write(&mut self, index: &Self::Index, value: Self::Value) -> Result<()>;

    fn get_solver(&self) -> Self::SolverRef;

    fn change_solver(&mut self, new_solver: Self::SolverRef);
}

Trait for things which can act like ‘memories’, that is, maps from bitvector (addresses) to bitvector (values)

Associated Types

type SolverRef: SolverRef<BV = Self::Index>[src]

type Index: BV<SolverRef = Self::SolverRef>[src]

type Value: BV[src]

Loading content...

Required methods

fn new_uninitialized(
    solver: Self::SolverRef,
    null_detection: bool,
    name: Option<&str>,
    addr_bits: u32
) -> Self[src]

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

fn new_zero_initialized(
    solver: Self::SolverRef,
    null_detection: bool,
    name: Option<&str>,
    addr_bits: u32
) -> Self[src]

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’)

addr_bits: e.g. 64 for a Memory which uses 64-bit addresses

fn read(&self, index: &Self::Index, bits: u32) -> Result<Self::Value>[src]

Read any number (>0) of bits of memory, at any alignment. Returned BV will have size bits.

fn write(&mut self, index: &Self::Index, value: Self::Value) -> Result<()>[src]

Write any number (>0) of bits of memory, at any alignment.

fn get_solver(&self) -> Self::SolverRef[src]

Get a reference to the solver instance this Memory belongs to

fn change_solver(&mut self, new_solver: Self::SolverRef)[src]

Adapt the Memory to a new solver instance.

The new solver instance should have been created (possibly transitively) via SolverRef::duplicate() from the SolverRef this Memory was originally created with (or most recently changed to). Further, no new variables should have been added since the call to SolverRef::duplicate().

Loading content...

Implementors

impl Memory for haybale::cell_memory::Memory[src]

type SolverRef = Rc<Btor>

type Index = BV<Rc<Btor>>

type Value = BV<Rc<Btor>>

impl Memory for haybale::simple_memory::Memory[src]

type SolverRef = Rc<Btor>

type Index = BV<Rc<Btor>>

type Value = BV<Rc<Btor>>

Loading content...