Skip to main content

box_into_raw

vstd_extra::external::smart_ptr

Function box_into_raw 

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

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

    ),
},

A wrapper around Box::into_raw that also returns the permission to access the memory.

Soundness: it is unsound to create a ptr method for Box<T> that returns the raw pointer without the permission. As Verus only compares the value of the Box<T> for equality, so the following code will be wrongly verified:

let b1 = Box::new(1);
let b2 = Box::new(1);
assert(b1.ptr() == b2.ptr()); // this will be verified but is actually not true, as b1 and b2 are different allocations with different pointers.