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.

logic

requires

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

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

logic(law)

ensures

self.offset_logic(0) == self

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

Offset is associative

logic(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.

logic

fn sub_logic_refl(self)

logic(law)

ensures

self.sub_logic(self) == 0

fn sub_offset_logic(self, offset: Int)

logic(law)

ensures

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

ensures

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

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

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

logic(opaque)

requires

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

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)

logic(law)

ensures

self.offset_logic(0) == self

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

logic(law)

ensures

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

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

logic(opaque)

fn sub_logic_refl(self)

logic(law)

ensures

self.sub_logic(self) == 0

fn sub_offset_logic(self, offset: Int)

logic(law)

ensures

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

ensures

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

impl<T> SizedPointerExt<T> for *mut T

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

logic(open, inline)

(self as *const T).offset_logic(offset) as *mut T

requires

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

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)

logic(law)

ensures

self.offset_logic(0) == self

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

logic(law)

ensures

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

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

logic(open, inline)

(self as *const T).sub_logic(rhs as *const T)

fn sub_logic_refl(self)

logic(law)

ensures

self.sub_logic(self) == 0

fn sub_offset_logic(self, offset: Int)

logic(law)

ensures

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

ensures

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

Implementors