Type Alias vstd::rwlock::FieldType_RwLock_exc

source · 
pub type FieldType_RwLock_exc<V, Pred> = AtomicBool<FieldType_RwLock_inst<V, Pred>, flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>, InvariantPredicate_auto_RwLock_exc>;

Aliased Type§

struct FieldType_RwLock_exc<V, Pred> { /* private fields */ }

Implementations

source§

impl<K, G, Pred> AtomicBool<K, G, Pred>
where Pred: AtomicInvariantPredicate<K, bool, G>,

source

pub fn well_formed(&self) -> bool

// verusdoc_special_attr modes
// { "fn_mode": "open spec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "" }
// verusdoc_special_attr body
{ self.atomic_inv@.constant().1 == self.patomic.id() }
source

pub fn constant(&self) -> K

// verusdoc_special_attr modes
// { "fn_mode": "open spec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "" }
// verusdoc_special_attr body
{ self.atomic_inv@.constant().0 }
source

pub const fn new( verus_tmp_k: Ghost<K>, u: bool, verus_tmp_g: Tracked<G>, ) -> Self

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default","Default","Default"], "broadcast": false, "ret_name": "t" }
// verusdoc_special_attr requires
Pred::atomic_inv(k, u, g),
// verusdoc_special_attr ensures
t.well_formed() && t.constant() == k,
source

pub fn load(&self) -> bool

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "" }
// verusdoc_special_attr requires
self.well_formed(),
source

pub fn into_inner(self) -> (bool, Tracked<G>)

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "res" }
// verusdoc_special_attr requires
self.well_formed(),
// verusdoc_special_attr ensures
Pred::atomic_inv(self.constant(), res.0, res.1@),