Struct vstd::rwlock::RwLockToks::flag_rc
source · pub struct flag_rc<K, V, Pred: InvariantPredicate<K, V>> { /* private fields */ }
Implementations§
source§impl<K, V, Pred: InvariantPredicate<K, V>> flag_rc<K, V, Pred>
impl<K, V, Pred: InvariantPredicate<K, V>> flag_rc<K, V, Pred>
Trait Implementations§
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
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
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 }
}
Auto Trait Implementations§
impl<K, V, Pred> RefUnwindSafe for flag_rc<K, V, Pred>
impl<K, V, Pred> Send for flag_rc<K, V, Pred>
impl<K, V, Pred> Sync for flag_rc<K, V, Pred>
impl<K, V, Pred> Unpin for flag_rc<K, V, Pred>
impl<K, V, Pred> UnwindSafe for flag_rc<K, V, Pred>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more