Type Alias FieldType_RwLock_rc

pub type FieldType_RwLock_rc<V, Pred> = AtomicUsize<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

impl<K, G, Pred> AtomicUsize<K, G, Pred>

where Pred: AtomicInvariantPredicate<K, usize, G>,

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() }

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 }

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

pub fn load(&self) -> usize

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "" }

// verusdoc_special_attr requires
self.well_formed(),

pub fn into_inner(self) -> (usize, 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@),