pub trait NonNullAdditionalFns<T: PointeeSized> {
// Required methods
spec fn view_ptr_mut(self) -> *mut T;
spec fn cast_spec<U>(self) -> NonNull<U>;
spec fn dangling_spec() -> NonNull<T>;
broadcast proof fn lemma_addr_is_nonnull(self);
spec fn addr_spec(self) -> NonZeroUsize;
broadcast proof fn lemma_addr_view_eq_view_ptr_mut(self);
exec fn addr_v(self) -> NonZeroUsize;
}Required Methods§
Sourcespec fn view_ptr_mut(self) -> *mut T
spec fn view_ptr_mut(self) -> *mut T
Sourcespec fn dangling_spec() -> NonNull<T>
spec fn dangling_spec() -> NonNull<T>
Specification for NonNull::dangling().
Sourcebroadcast proof fn lemma_addr_is_nonnull(self)
broadcast proof fn lemma_addr_is_nonnull(self)
ensures
(#[trigger] self.view_ptr_mut())@.addr != 0,Type invariant: the address of the pointer is non-null.
Sourcespec fn addr_spec(self) -> NonZeroUsize
spec fn addr_spec(self) -> NonZeroUsize
Sourcebroadcast proof fn lemma_addr_view_eq_view_ptr_mut(self)
broadcast proof fn lemma_addr_view_eq_view_ptr_mut(self)
ensures
(#[trigger] self.addr_spec()).view() == self.view_ptr_mut()@.addr,Sourceexec fn addr_v(self) -> NonZeroUsize
exec fn addr_v(self) -> NonZeroUsize
returns
self.addr_spec(),A wrapper of NonNull::addr in std, here we use our own NonZeroUsize
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<T: PointeeSized> NonNullAdditionalFns<T> for NonNull<T>
impl<T: PointeeSized> NonNullAdditionalFns<T> for NonNull<T>
Source§uninterp fn view_ptr_mut(self) -> *mut T
uninterp fn view_ptr_mut(self) -> *mut T
Source§uninterp fn dangling_spec() -> NonNull<T>
uninterp fn dangling_spec() -> NonNull<T>
Source§proof fn lemma_addr_is_nonnull(self)
proof fn lemma_addr_is_nonnull(self)
Source§open spec fn addr_spec(self) -> NonZeroUsize
open spec fn addr_spec(self) -> NonZeroUsize
{ NonZeroUsize::nonzero_usize_from_usize(self.view_ptr_mut()@.addr) }