Trait PtrPointsToTrait 

pub trait PtrPointsToTrait {
    type Ptr;
    type Target;

    // Required methods
    spec fn ptr(self) -> *mut Self::Target;
    spec fn view_target(self) -> Self::Target;
}

A verification-only trait that abstracts the permission that tracks both the pointer and the value it points to.

Required Associated Types

type Ptr

The type of the pointer.

type Target

The type of the value that the pointer points to.

Required Methods

spec fn ptr(self) -> *mut Self::Target

spec fn view_target(self) -> Self::Target

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<T> PtrPointsToTrait for ArcPointsTo<T>

type Ptr = Arc<T>

type Target = T

impl<T> PtrPointsToTrait for BoxPointsTo<T>

type Ptr = Box<T>

type Target = T