Function vstd::raw_ptr::deallocate

source · 
pub exec fn deallocate(
    p: *mut u8,
    size: usize,
    align: usize,
    verus_tmp_pt: Tracked<PointsToRaw>,
    verus_tmp_dealloc: Tracked<Dealloc>
)
Expand description
requires
dealloc.addr() == p.addr(),
dealloc.size() == size,
dealloc.align() == align,
dealloc.provenance() == pt.provenance(),
pt.is_range(dealloc.addr() as int, dealloc.size() as int),
p@.provenance == dealloc.provenance(),

Deallocate with the global allocator.