Skip to main content

arc_from_raw

vstd_extra::external::smart_ptr

Function arc_from_raw 

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

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.