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