Function pre::std::slice::from_raw_parts_mut

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

std::slice::from_raw_parts_mut with preconditions.

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

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

This function has preconditions

This function has the following preconditions generated by pre attributes:

• the pointer data must be valid for reads and writes
• 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 accessed by any pointer other than the returned slice for the duration of 'a
• 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+w),
    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 accessed by any pointer other than the returned slice for the duration of `'a`",
    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_mut(/* parameters omitted */);