Module vstd::simple_pptr

Re-exports

• pub use raw_ptr::MemContents;

Structs

• PPtr
  PPtr (which stands for “permissioned pointer”) is a wrapper around a raw pointer to a heap-allocated V. This is designed to be simpler to use that Verus’s more general pointer support, but also to serve as a better introductory point. Historically, PPtr was positioned as a “trusted primitive” of Verus, but now, it is implemented and verified from the more general pointer support, which operates on similar principles, but which is much precise to Rust’s pointer semantics.
• PointsTo
  A tracked ghost object that gives the user permission to dereference a pointer for reading or writing, or to free the memory at that pointer.