Trait SizedPointerExt 

pub trait SizedPointerExt<T>: PointerExt<T> {
    // Required methods
    fn offset_logic(self, offset: Int) -> Self;
    fn offset_logic_zero(self);
    fn offset_logic_assoc(self, offset1: Int, offset2: Int);
    fn sub_logic(self, rhs: Self) -> Int;
    fn sub_logic_refl(self);
    fn sub_offset_logic(self, offset: Int);
}

Extension methods for *const T where T: Sized.

Required Methods

fn offset_logic(self, offset: Int) -> Self

Pointer offset in logic

The current contract only describes the effect on addr_logic in the absence of overflow.

requires

self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@

ensures

result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>()

fn offset_logic_zero(self)

Offset by zero is the identity

(law)

ensures

self.offset_logic(0) == self

fn offset_logic_assoc(self, offset1: Int, offset2: Int)

Offset is associative

(law)

ensures

self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2)

fn sub_logic(self, rhs: Self) -> Int

Pointer subtraction

Note: we don’t have ptr1 + (ptr2 - ptr1) == ptr2, because pointer subtraction discards provenance.

fn sub_logic_refl(self)

(law)

ensures

self.sub_logic(self) == 0

fn sub_offset_logic(self, offset: Int)

(law)

ensures

self.offset_logic(offset).sub_logic(self) == offset

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<T> SizedPointerExt<T> for *const T

fn offset_logic(self, offset: Int) -> Self

(opaque)

requires

self.addr_logic()@ + offset * size_of_logic::<T>() < usize::MAX@

ensures

result.addr_logic()@ == self.addr_logic()@ + offset * size_of_logic::<T>()

fn offset_logic_zero(self)

(law)

ensures

self.offset_logic(0) == self

fn offset_logic_assoc(self, offset1: Int, offset2: Int)

(law)

ensures

self.offset_logic(offset1).offset_logic(offset2) == self.offset_logic(offset1 + offset2)

fn sub_logic(self, rhs: Self) -> Int

(opaque)

fn sub_logic_refl(self)

(law)

ensures

self.sub_logic(self) == 0

fn sub_offset_logic(self, offset: Int)

(law)

ensures

self.offset_logic(offset).sub_logic(self) == offset

Implementors