box_from_raw

vstd_extra::external::smart_ptr

Function box_from_raw 

Source 
pub unsafe exec fn box_from_raw<T>(
    ptr: *mut T,
tracked     points_to: Tracked<PointsTo<T>>,
tracked     dealloc: Tracked<Option<Dealloc>>,
) -> ret : Box<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,
match dealloc@ {
    Some(dealloc) => (
        &&& vstd::layout::size_of::<T>() > 0
        &&& dealloc.addr() == ptr@.addr
        &&& dealloc.size() == vstd::layout::size_of::<T>()
        &&& dealloc.align() == vstd::layout::align_of::<T>()
        &&& dealloc.provenance() == ptr@.provenance
        &&& valid_layout(size_of::<T>(), align_of::<T>())

    ),
    None => (
        &&& vstd::layout::size_of::<T>() == 0

    ),
},
ensures
box_pointer_spec(ret) == ptr,