Function pre::std::ptr::swap_nonoverlapping

pub unsafe fn swap_nonoverlapping<T>(x: *mut T, y: *mut T, count: usize)

std::ptr::swap_nonoverlapping with preconditions.

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

You should also read the Safety section on the documentation of std::ptr::swap_nonoverlapping.

This function has preconditions

This function has the following preconditions generated by pre attributes:

• the pointer x must be valid for reads and writes
• the pointer y must be valid for reads and writes
• x is valid for count * size_of::<T>() bytes
• y is valid for count * size_of::<T>() bytes
• the pointer x must have a proper alignment for its type
• the pointer y must have a proper alignment for its type
• the memory regions of size count * size_of::<T> pointed to by x and y do not overlap

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

#[assure(
    valid_ptr(x, r+w),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    valid_ptr(y, r+w),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`x` is valid for `count * size_of::<T>()` bytes",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`y` is valid for `count * size_of::<T>()` bytes",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    proper_align(x),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    proper_align(y),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "the memory regions of size `count * size_of::<T>` pointed to by `x` and `y` do not overlap",
    reason = "<specify the reason why you can assure this here>"
)]
swap_nonoverlapping(/* parameters omitted */);