Trait NonNullAdditionalFnsMore 

pub trait NonNullAdditionalFnsMore<T>: NonNullAdditionalFns<T>
where
    T: PointeeSized,
{
    // Required methods
    spec fn with_addr_spec(self, addr: NonZeroUsize) -> NonNull<T>;
    proof fn lemma_with_addr_properties(self, addr: NonZeroUsize);
    exec fn with_addr_v(self, addr: NonZeroUsize) -> ret : NonNull<T>;
}

Required Methods

spec fn with_addr_spec(self, addr: NonZeroUsize) -> NonNull<T>

proof fn lemma_with_addr_properties(self, addr: NonZeroUsize)

ensures

self.with_addr_spec(addr).view_ptr_mut()@.metadata == self.view_ptr_mut()@.metadata,

self.with_addr_spec(addr).view_ptr_mut()@.provenance == self.view_ptr_mut()@.provenance,

self.with_addr_spec(addr).view_ptr_mut()@.addr == addr.view(),

exec fn with_addr_v(self, addr: NonZeroUsize) -> ret : NonNull<T>

returns

self.with_addr_spec(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> NonNullAdditionalFnsMore<T> for NonNull<T>

uninterp spec fn with_addr_spec(self, addr: NonZeroUsize) -> NonNull<T>

proof fn lemma_with_addr_properties(self, addr: NonZeroUsize)

exec fn with_addr_v(self, addr: NonZeroUsize) -> ret : NonNull<T>

Implementors