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.