Trait gf::ai::state::SpaceState

pub trait SpaceState<A, V: Bottom>: ConstSpaceState<A, V> {
    fn store(&mut self, span: SpaceSpan<A>, value: V) -> (Option<()>, V);

    fn store_result(
        &mut self, 
        span: SpaceSpan<A>, 
        value: V
    ) -> Result<Option<()>, V> { ... }
}

🟢 An abstract state of an address space with A for addresses and V for values.

Required methods

fn store(&mut self, span: SpaceSpan<A>, value: V) -> (Option<()>, V)

Store to the space.

This method returns a tuple where the first element is the successful store indicator in terms of the trivial lattice {⊥, ⊤}, and the second one is the error context state.

Loading content...

Provided methods

fn store_result(
    &mut self,
    span: SpaceSpan<A>,
    value: V
) -> Result<Option<()>, V>

Store to the space returning a Result.

This returns Ok when the error context state is ⊥, and otherwise the error context state wrapped in Err.

Loading content...

Implementors

impl SpaceState<FlatLattice<BitVec>, FlatLattice<Expr>> for SymbolicSpaceState

fn store(
    &mut self,
    span: SpaceSpan<FlatLattice<BitVec>>,
    value: FlatLattice<Expr>
) -> (Option<()>, FlatLattice<Expr>)

impl SpaceState<FlatLattice<BitVec>, FlatLattice<BitVec>> for ConcreteSpaceState

fn store(
    &mut self,
    span: SpaceSpan<FlatLattice<BitVec>>,
    value: FlatLattice<BitVec>
) -> (Option<()>, FlatLattice<BitVec>)

impl SpaceState<BitVec, FlatLattice<Expr>> for SymbolicSpaceState

fn store(
    &mut self,
    span: SpaceSpan<BitVec>,
    value: FlatLattice<Expr>
) -> (Option<()>, FlatLattice<Expr>)

impl SpaceState<BitVec, FlatLattice<BitVec>> for ConcreteSpaceState

fn store(
    &mut self,
    span: SpaceSpan<BitVec>,
    value: FlatLattice<BitVec>
) -> (Option<()>, FlatLattice<BitVec>)

impl<A: IntoU128> SpaceState<A, FlatLattice<Expr>> for SymbolicSpaceState

fn store(
    &mut self,
    span: SpaceSpan<A>,
    value: FlatLattice<Expr>
) -> (Option<()>, FlatLattice<Expr>)

impl<A: IntoU128> SpaceState<A, FlatLattice<BitVec>> for ConcreteSpaceState

fn store(
    &mut self,
    span: SpaceSpan<A>,
    value: FlatLattice<BitVec>
) -> (Option<()>, FlatLattice<BitVec>)

Loading content...