Trait NonNullAdditionalFns 

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

Required Methods

spec fn view_ptr_mut(self) -> *mut T

spec fn cast_spec<U>(self) -> NonNull<U>

Specification for NonNull::cast.

spec fn dangling_spec() -> NonNull<T>

Specification for NonNull::dangling().

broadcast proof fn lemma_addr_is_nonnull(self)

ensures

!(#[trigger] self.view_ptr_mut()).is_null(),

Type invariant: the address of the pointer is non-null.

spec fn addr_spec(self) -> NonZeroUsize

broadcast proof fn lemma_addr_view_eq_view_ptr_mut(self)

ensures

(#[trigger] self.addr_spec()).view() == self.view_ptr_mut().addr(),

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<T: PointeeSized> NonNullAdditionalFns<T> for NonNull<T>

uninterp spec fn view_ptr_mut(self) -> *mut T

uninterp spec fn cast_spec<U>(self) -> NonNull<U>

uninterp spec fn dangling_spec() -> NonNull<T>

proof fn lemma_addr_is_nonnull(self)

open spec fn addr_spec(self) -> NonZeroUsize

{ nonzero_from_primitive(self.view_ptr_mut()@.addr) }

proof fn lemma_addr_view_eq_view_ptr_mut(self)

Implementors