Trait PtrAddExt 

pub trait PtrAddExt<'a, T> {
    // Required methods
    unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self;
    unsafe fn offset_live(
        self,
        offset: isize,
        live: Ghost<PtrLive<'a, T>>,
    ) -> Self;
}

Pointer offsets with PtrLive permissions.

This trait provides wrappers around the offset functions:

• <*const T>::add
• <*const T>::offset
• <*mut T>::add
• <*mut T>::offset

with ghost permission tokens (PtrLive) that allow proving their safety conditions.

Safety

Source: https://doc.rust-lang.org/core/intrinsics/fn.offset.html

If the computed offset is non-zero, then both the starting and resulting pointer must be either in bounds or at the end of an allocation. If either pointer is out of bounds or arithmetic overflow occurs then this operation is undefined behavior.

The preconditions ensure that the live witness contains the range between dst and dst + offset, which prevents out-of-bounds access and overflow.

Required Methods

unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self

Implementations refine this with a non-trivial precondition.

requires

false

unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self

Implementations refine this with a non-trivial precondition.

requires

false

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

impl<'a, T> PtrAddExt<'a, T> for *const T

unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self

Permission-aware wrapper around <*const T>::add

erasure

<*const T>::add

requires

live.contains_range(self, offset@)

ensures

result == self.offset_logic(offset@)

unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self

Permission-aware wrapper around <*const T>::offset

erasure

<*const T>::offset

requires

live.contains_range(self, offset@)

ensures

result == self.offset_logic(offset@)

impl<'a, T> PtrAddExt<'a, T> for *mut T

unsafe fn add_live(self, offset: usize, live: Ghost<PtrLive<'a, T>>) -> Self

Permission-aware wrapper around <*mut T>::add

erasure

<*mut T>::add

requires

live.contains_range(self, offset@)

ensures

result == self.offset_logic(offset@)

unsafe fn offset_live(self, offset: isize, live: Ghost<PtrLive<'a, T>>) -> Self

Permission-aware wrapper around <*mut T>::offset

erasure

<*mut T>::offset

requires

live.contains_range(self, offset@)

ensures

result == self.offset_logic(offset@)

Implementors