vstd::atomic_ghost

Trait AtomicInvariantPredicate

Source 
pub trait AtomicInvariantPredicate<K, V, G> {
    // Required method
    spec fn atomic_inv(k: K, v: V, g: G) -> bool;
}

Required Methods§

Source

spec fn atomic_inv(k: K, v: V, g: G) -> bool

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§

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§

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