Struct vstd::atomic::PAtomicU16
source · pub struct PAtomicU16 { /* private fields */ }
Implementations§
source§impl PAtomicU16
impl PAtomicU16
sourcepub const exec fn new(i: u16) -> (PAtomicU16, Tracked<PermissionU16>)
pub const exec fn new(i: u16) -> (PAtomicU16, Tracked<PermissionU16>)
ensures
equal(
res.1@.view(),
PermissionDataU16 {
patomic: res.0.id(),
value: i,
},
),
sourcepub exec fn load(&self, verus_tmp_perm: Tracked<&PermissionU16>) -> u16
pub exec fn load(&self, verus_tmp_perm: Tracked<&PermissionU16>) -> u16
requires
equal(self.id(), perm.view().patomic),
ensuresequal(perm.view().value, ret),
sourcepub exec fn store(&self, verus_tmp_perm: Tracked<&mut PermissionU16>, v: u16)
pub exec fn store(&self, verus_tmp_perm: Tracked<&mut PermissionU16>, v: u16)
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(perm.view().value, v) && equal(self.id(), perm.view().patomic),
sourcepub exec fn compare_exchange(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
current: u16,
new: u16
) -> Result<u16, u16>
pub exec fn compare_exchange( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, current: u16, new: u16 ) -> Result<u16, u16>
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(self.id(), perm.view().patomic)
&& match ret {
Result::Ok(r) => {
current == old(perm).view().value && equal(perm.view().value, new)
&& equal(r, old(perm).view().value)
}
Result::Err(r) => {
current != old(perm).view().value
&& equal(perm.view().value, old(perm).view().value)
&& equal(r, old(perm).view().value)
}
},
sourcepub exec fn compare_exchange_weak(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
current: u16,
new: u16
) -> Result<u16, u16>
pub exec fn compare_exchange_weak( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, current: u16, new: u16 ) -> Result<u16, u16>
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(self.id(), perm.view().patomic)
&& match ret {
Result::Ok(r) => {
current == old(perm).view().value && equal(perm.view().value, new)
&& equal(r, old(perm).view().value)
}
Result::Err(r) => {
equal(perm.view().value, old(perm).view().value)
&& equal(r, old(perm).view().value)
}
},
sourcepub exec fn swap(&self, verus_tmp_perm: Tracked<&mut PermissionU16>, v: u16) -> u16
pub exec fn swap(&self, verus_tmp_perm: Tracked<&mut PermissionU16>, v: u16) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(perm.view().value, v) && equal(old(perm).view().value, ret)
&& equal(self.id(), perm.view().patomic),
sourcepub exec fn into_inner(self, verus_tmp_perm: Tracked<PermissionU16>) -> u16
pub exec fn into_inner(self, verus_tmp_perm: Tracked<PermissionU16>) -> u16
requires
equal(self.id(), perm.view().patomic),
ensuresequal(perm.view().value, ret),
sourcepub exec fn fetch_add_wrapping(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_add_wrapping( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value as int == wrapping_add_u16(old(perm).view().value as int, n as int),
sourcepub exec fn fetch_sub_wrapping(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_sub_wrapping( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value as int == wrapping_sub_u16(old(perm).view().value as int, n as int),
sourcepub exec fn fetch_add(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_add( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
(<u16>::MIN as int) <= old(perm).view().value + n,
old(perm).view().value + n <= (<u16>::MAX as int),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value == old(perm).view().value + n,
sourcepub exec fn fetch_sub(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_sub( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
(<u16>::MIN as int) <= old(perm).view().value - n,
old(perm).view().value - n <= <u16>::MAX as int,
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value == old(perm).view().value - n,
sourcepub exec fn fetch_and(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_and( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value == (old(perm).view().value & n),
sourcepub exec fn fetch_or(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_or( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value == (old(perm).view().value | n),
sourcepub exec fn fetch_xor(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_xor( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value == (old(perm).view().value ^ n),
sourcepub exec fn fetch_nand(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_nand( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value == !(old(perm).view().value & n),
sourcepub exec fn fetch_max(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_max( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value
== (if old(perm).view().value > n { old(perm).view().value } else { n }),
sourcepub exec fn fetch_min(
&self,
verus_tmp_perm: Tracked<&mut PermissionU16>,
n: u16
) -> u16
pub exec fn fetch_min( &self, verus_tmp_perm: Tracked<&mut PermissionU16>, n: u16 ) -> u16
requires
equal(self.id(), old(perm).view().patomic),
ensuresequal(old(perm).view().value, ret),
perm.view().patomic == old(perm).view().patomic,
perm.view().value
== (if old(perm).view().value < n { old(perm).view().value } else { n }),
Auto Trait Implementations§
impl RefUnwindSafe for PAtomicU16
impl Send for PAtomicU16
impl Sync for PAtomicU16
impl Unpin for PAtomicU16
impl UnwindSafe for PAtomicU16
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