Skip to main content

PtrPointsToTrait

vstd_extra::external::smart_ptr

Trait PtrPointsToTrait 

Source 
pub trait PtrPointsToTrait {
    type Ptr;
    type Target;

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

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

Required Associated Types§

Source

type Ptr

The type of the pointer.

Source

type Target

The type of the value that the pointer points to.

Required Methods§

Source

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

Source

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

Implementors§