Skip to main content

arc_into_raw

vstd_extra::external::smart_ptr

Function arc_into_raw 

Source 
pub exec fn arc_into_raw<T>(p: Arc<T>) -> ret : *const T
Expand description
with
->
perm: Tracked<ArcPointsTo<T>>,
ensures
ret == perm@.ptr(),
perm@.ptr().addr() != 0,
perm@.is_init(),
perm@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
perm@.value() == *p,

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

Soundness: the soundness concern is similar to box_into_raw.