box_into_raw

vstd_extra::external::smart_ptr

Function box_into_raw 

Source 
pub exec fn box_into_raw<T>(
    b: Box<T>,
) -> (*mut T, Tracked<PointsTo<T>>, Tracked<Option<Dealloc>>)
Expand description
ensures
ret == box_pointer_spec(b),
ret == perm@.ptr(),
perm@.ptr().addr() != 0,
perm@.is_init(),
perm@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
match dealloc@ {
    Some(dealloc) => (
        &&& vstd::layout::size_of::<T>() > 0
        &&& dealloc.addr() == perm@.ptr().addr()
        &&& dealloc.size() == vstd::layout::size_of::<T>()
        &&& dealloc.align() == vstd::layout::align_of::<T>()
        &&& dealloc.provenance() == perm@.ptr()@.provenance
        &&& valid_layout(size_of::<T>(), align_of::<T>())

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

    ),
},