Function pre::std::slice::from_raw_parts

pub unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T]

std::slice::from_raw_parts with preconditions.

This function behaves exactly like std::slice::from_raw_parts, but also has preconditions checked by pre.

You should also read the Safety section on the documentation of std::slice::from_raw_parts.

This function has preconditions

This function has the following preconditions generated by pre attributes:

• the pointer data must be valid for reads
• the pointer data must have a proper alignment for its type
• the allocated object at data is valid for len * mem::size_of::<T>() bytes
• the memory referenced by the returned slice is not mutated by any pointer for the duration of 'a, except inside a contained UnsafeCell
• len * :: core :: mem :: size_of :: < T > () <= isize :: MAX as usize

To call the function you need to assure that the preconditions hold:

#[assure(
    valid_ptr(data, r),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    proper_align(data),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "the allocated object at `data` is valid for `len * mem::size_of::<T>()` bytes",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "the memory referenced by the returned slice is not mutated by any pointer for the duration of `\'a`, except inside a contained `UnsafeCell`",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    len * :: core :: mem :: size_of :: < T > () <= isize :: MAX as usize,
    reason = "<specify the reason why you can assure this here>"
)]
from_raw_parts(/* parameters omitted */);