Module vstd::raw_ptr

source ·
Expand description

Tools and reasoning principles for raw pointers. The tools here are meant to address “real Rust pointers, including all their subtleties on the Rust Abstract Machine, to the largest extent that is reasonable.”

For a gentler introduction to some of the concepts here, see PPtr, which uses a much-simplified pointer model.

§Pointer model

A pointer consists of an address (ptr.addr() or ptr as usize), a provenance ptr@.provenance, and a ptr@.metadata (which is trivial except for pointers to non-sized types). Note that in spec code, pointer equality requires all 3 to be equal, whereas runtime equality (eq) only compares addresses and metadata.

*mut T vs. *const T doesn’t have any semantic different and Verus treats them as the same; they can be seamlessly cast to and fro.

Structs§

  • Dealloc
    Permission to perform a deallocation with the global allocator
  • DeallocData
  • DynMetadata
  • IsExposed
  • PointsTo
    Permission to access possibly-initialized, typed memory.
  • PointsToData
  • PointsToRaw
    PointsToRaw Variable-sized uninitialized memory.
  • Provenance
  • PtrData
    Model of a pointer *mut T or *const T in Rust’s abstract machine
  • SharedReference
    This is meant to be a replacement for &'a T that allows Verus to keep track of not just the T value but the pointer as well. It would be better to get rid of this and use normal reference types &'a T, but there are a lot of unsolved implementation questions. The existence of SharedReference<'a, T> is a stop-gap.

Enums§

Functions§