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>;
    exec fn map_addr_v<F: FnOnce(NonZeroUsize) -> NonZeroUsize>(
        self,
        f: F,
    ) -> 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),

exec fn map_addr_v<F: FnOnce(NonZeroUsize) -> NonZeroUsize>(self, f: F) -> ret : NonNull<T>

requires

f.requires((self.addr_spec(),)),

ensures

ret.view_ptr_mut()@.metadata == self.view_ptr_mut()@.metadata,

ret.view_ptr_mut()@.provenance == self.view_ptr_mut()@.provenance,

f.ensures((self.addr_spec(),), ret.addr_spec()),

A wrapper of NonNull::map_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".

Implementations on Foreign Types

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

exec fn map_addr_v<F: FnOnce(NonZeroUsize) -> NonZeroUsize>(self, f: F) -> ret : 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