Struct vstd::prelude::Tracked

pub struct Tracked<A> { /* private fields */ }

Implementations§

§

impl<A> Tracked<A>

pub fn view(self) -> A

pub fn new(_a: A) -> Tracked<A>

pub fn get(self) -> A

pub fn borrow(&self) -> &A

pub fn borrow_mut(&mut self) -> &mut A

Trait Implementations§

source §

impl<V, Pred: RwLockPredicate<V>> AtomicInvariantPredicate<Tracked<Instance<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>, bool, flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>> for InvariantPredicate_auto_RwLock_exc

source §

open spec fn atomic_inv( declare_struct_with_invariants_tmp_k: FieldType_RwLock_inst<V, Pred>, declare_struct_with_invariants_tmp_v: bool, declare_struct_with_invariants_tmp_g: flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>> ) -> bool

{
    let inst = declare_struct_with_invariants_tmp_k;
    let v = declare_struct_with_invariants_tmp_v;
    let g = declare_struct_with_invariants_tmp_g;
    { g@.instance == inst@ && g@.value == v }
}

source §

impl<V, Pred: RwLockPredicate<V>> AtomicInvariantPredicate<Tracked<Instance<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>, u64, flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>> for InvariantPredicate_auto_RwLock_rc

source §

open spec fn atomic_inv( declare_struct_with_invariants_tmp_k: FieldType_RwLock_inst<V, Pred>, declare_struct_with_invariants_tmp_v: u64, declare_struct_with_invariants_tmp_g: flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>> ) -> bool

{
    let inst = declare_struct_with_invariants_tmp_k;
    let v = declare_struct_with_invariants_tmp_v;
    let g = declare_struct_with_invariants_tmp_g;
    { g@.instance == inst@ && g@.value == v }
}

§