Module ptr 

Structs

PtrDeepModel

We conservatively model raw pointers as having an address plus some hidden metadata.

Traits

PointerExt

Extension trait for pointers

SizedPointerExt

Extension methods for *const T where T: Sized.

SlicePointerExt

Extension methods for *const [T]

Functions

extern_spec_T_Clone__ptrconst_T_clone

extern spec for [pointer<T>::clone]

extern_spec_T_Clone__ptrmut_T_clone

extern spec for [pointer<T>::clone]

extern_spec_T__ptrconst_T_addr

extern spec for pointer<T>::addr

extern_spec_T__ptrconst_T_cast

extern spec for pointer<T>::cast<U>

extern_spec_T__ptrconst_T_is_aligned

extern spec for pointer<T>::is_aligned

extern_spec_T__ptrconst_T_is_aligned_to

extern spec for pointer<T>::is_aligned_to

extern_spec_T__ptrconst_T_is_null

extern spec for pointer<T>::is_null

extern_spec_T__ptrconst__slice_T_len

extern spec for pointer<slice<T>>::len

extern_spec_T__ptrmut_T_addr

extern spec for pointer<T>::addr

extern_spec_T__ptrmut_T_cast

extern spec for pointer<T>::cast<U>

extern_spec_T__ptrmut_T_is_aligned

extern spec for pointer<T>::is_aligned

extern_spec_T__ptrmut_T_is_aligned_to

extern spec for pointer<T>::is_aligned_to

extern_spec_T__ptrmut_T_is_null

extern spec for pointer<T>::is_null

extern_spec_T__ptrmut__slice_T_len

extern spec for pointer<slice<T>>::len

extern_spec_core_ptr_addr_eq

extern spec for ::core::ptr::addr_eq<T, U>

extern_spec_core_ptr_metadata

extern spec for ::core::ptr::metadata<T>

extern_spec_core_ptr_null

extern spec for ::core::ptr::null<T>

extern_spec_core_ptr_null_mut

extern spec for ::core::ptr::null_mut<T>

extern_spec_core_ptr_read_volatile^⚠

extern spec for ::core::ptr::read_volatile<T>

extern_spec_core_ptr_slice_from_raw_parts

extern spec for ::core::ptr::slice_from_raw_parts<T>

extern_spec_core_ptr_slice_from_raw_parts_mut

extern spec for ::core::ptr::slice_from_raw_parts_mut<T>

is_aligned_logic

Whether a pointer is aligned.

metadata_logic

Metadata of a pointer in logic.

metadata_matches

Check that a value is compatible with some metadata.