Skip to main content

NonNullAdditionalFnsMore

vstd_extra::external::nonnull

Trait NonNullAdditionalFnsMore 

Source 
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§

Source

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

Source

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(),
Source

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

returns
self.with_addr_spec(addr),
Source

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", so this trait is not object safe.

Implementations on Foreign Types§

Source§

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

Source§

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

Source§

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

Source§

proof fn lemma_with_addr_properties(self, addr: NonZeroUsize)

Source§

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

Implementors§