Module smart_ptr 

Structs

ArcPointsTo

For Arc<T>, the into_raw method gives shared access to the memory, and the reference count is not decreased, so the value will not be deallocated until we convert back to Arc<T> and drop it. See https://doc.rust-lang.org/src/alloc/sync.rs.html#1480.

BoxPointsTo

For Box<T>, the into_raw method gives you the ownership of the memory

BoxPointsToRef

A permission that is equivalent to &BoxPointsTo<T>.

Traits

PtrPointsToTrait

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

Functions

arc_from_raw^⚠

According to the documentation, Arc::from_raw allows transmuting between different types as long as the pointer has the same size and alignment. In verification this responsibility is dispatched to casting the PointsTo<T> appropriately, which is not handled here.

arc_into_raw

A wrapper around Arc::into_raw that also returns the permission to access the memory.

box_from_raw^⚠

box_into_raw

A wrapper around Box::into_raw that also returns the permission to access the memory.