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.