Skip to main content

RawPtrPerm

vstd_extra::external::smart_ptr

Trait RawPtrPerm 

Source 
pub trait RawPtrPerm {
    type Ptr;
    type Target;

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

A verification-only trait that abstracts the permission that can be obtained from a raw pointer.

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 addr(self) -> usize

Implementors§