pub exec fn deallocate(
p: *mut u8,
size: usize,
align: usize,
Tracked(pt): Tracked<PointsToRaw>,
Tracked(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.