Skip to main content

box_from_raw

vstd_extra::external::smart_ptr

Function box_from_raw 

Source 
pub unsafe exec fn box_from_raw<T>(ptr: *mut T) -> ret : Box<T>
Expand description
with
Tracked(points_to): Tracked<PointsTo<T>>,
Tracked(dealloc): Tracked<Option<Dealloc>>,
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
*ret == points_to.value(),