vstd::raw_ptr

Function allocate

Source 
pub exec fn allocate(
    size: usize,
    align: usize,
) -> pt : (*mut u8, Tracked<PointsToRaw>, Tracked<Dealloc>)
Expand description
requires
valid_layout(size, align),
size != 0,
ensures
pt.1@.is_range(pt.0.addr() as int, size as int),
pt.0.addr() + size <= usize::MAX + 1,
pt.2@@
    == (DeallocData {
        addr: pt.0.addr(),
        size: size as nat,
        align: align as nat,
        provenance: pt.1@.provenance(),
    }),
pt.0.addr() as int % align as int == 0,
pt.0@.provenance == pt.1@.provenance(),

Allocate with the global allocator. The precondition should be consistent with the documented safety conditions on alloc. Returns a pointer with a corresponding PointsToRaw and Dealloc permissions.