pub struct PointsTo<V> { /* private fields */ }
Expand description
Implementations§
source§impl<V> PointsTo<V>
impl<V> PointsTo<V>
sourcepub uninterp fn mem_contents(&self) -> MemContents<V>
pub uninterp fn mem_contents(&self) -> MemContents<V>
The contents of the cell, either unitialized or initialized to some V
.
sourcepub open spec fn view(self) -> PointsToData<V>
pub open spec fn view(self) -> PointsToData<V>
{
PointsToData {
pcell: self.id(),
value: option_from_mem_contents(self.mem_contents()),
}
}
sourcepub open spec fn opt_value(&self) -> Option<V>
👎Deprecated: use mem_contents() instead
pub open spec fn opt_value(&self) -> Option<V>
{
match self.mem_contents() {
MemContents::Init(value) => Some(value),
MemContents::Uninit => None,
}
}
sourcepub open spec fn is_init(&self) -> bool
pub open spec fn is_init(&self) -> bool
{ self.mem_contents().is_init() }
Is this cell initialized?
Auto Trait Implementations§
impl<V> Freeze for PointsTo<V>
impl<V> RefUnwindSafe for PointsTo<V>where
V: RefUnwindSafe,
impl<V> Send for PointsTo<V>where
V: Send,
impl<V> Sync for PointsTo<V>where
V: Sync,
impl<V> Unpin for PointsTo<V>where
V: Unpin,
impl<V> UnwindSafe for PointsTo<V>where
V: UnwindSafe,
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