Type Alias vstd::rwlock::FieldType_RwLock_rc

source · 
pub type FieldType_RwLock_rc<V, Pred> = AtomicU64<FieldType_RwLock_inst<V, Pred>, flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>, InvariantPredicate_auto_RwLock_rc>;

Aliased Type§

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

Implementations

source§

impl<K, G, Pred> AtomicU64<K, G, Pred>
where Pred: AtomicInvariantPredicate<K, u64, 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
{ @.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
{ @.constant().0 }
source

pub const fn new(verus_tmp_k: Ghost<K>, u: u64, 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) -> u64

// 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) -> (u64, 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, @),