vstd::raw_ptr

Function 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.

The Dealloc permission ensures that the documented safety conditions on dealloc are satisfied; by also giving up permission of the PointsToRaw permission, we ensure there can be no use-after-free bug as a result of this deallocation. In order to do so, the parameters of the PointsToRaw and Dealloc permissions must match the parameters of the deallocation.