Add assumptions that the pointer is non-null
This commit is contained in:
@@ -933,12 +933,26 @@ trait RcBoxPtr<T> {
|
|||||||
|
|
||||||
impl<T> RcBoxPtr<T> for Rc<T> {
|
impl<T> RcBoxPtr<T> for Rc<T> {
|
||||||
#[inline(always)]
|
#[inline(always)]
|
||||||
fn inner(&self) -> &RcBox<T> { unsafe { &(**self._ptr) } }
|
fn inner(&self) -> &RcBox<T> {
|
||||||
|
unsafe {
|
||||||
|
// Safe to assume this here, as if it weren't true, we'd be breaking
|
||||||
|
// the contract anyway
|
||||||
|
assume(!self._ptr.is_null());
|
||||||
|
&(**self._ptr)
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<T> RcBoxPtr<T> for Weak<T> {
|
impl<T> RcBoxPtr<T> for Weak<T> {
|
||||||
#[inline(always)]
|
#[inline(always)]
|
||||||
fn inner(&self) -> &RcBox<T> { unsafe { &(**self._ptr) } }
|
fn inner(&self) -> &RcBox<T> {
|
||||||
|
unsafe {
|
||||||
|
// Safe to assume this here, as if it weren't true, we'd be breaking
|
||||||
|
// the contract anyway
|
||||||
|
assume(!self._ptr.is_null());
|
||||||
|
&(**self._ptr)
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
|
|||||||
Reference in New Issue
Block a user