Function vstd::raw_ptr::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.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@.metadata == Metadata::Thin,
pt.0@.provenance == pt.1@.provenance(),

Allocate with the global allocator. Precondition should be consistent with the documented safety conditions on alloc.