arc_from_raw

vstd_extra::external::smart_ptr

Function arc_from_raw 

Source 
pub unsafe exec fn arc_from_raw<T>(
    ptr: *const T,
tracked     points_to: Tracked<ArcPointsTo<T>>,
) -> ret : Arc<T>
Expand description
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
arc_pointer_spec(ret) == ptr,

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.