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.