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.