Function pre::std::ptr::copy

pub unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize)

std::ptr::copy with preconditions.

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

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

This function has preconditions

This function has the following preconditions generated by pre attributes:

• the pointer src must be valid for reads
• the pointer dst must be valid for writes
• src is valid for count * size_of::<T>() bytes
• dst is valid for count * size_of::<T>() bytes
• the pointer src must have a proper alignment for its type
• the pointer dst must have a proper alignment for its type
• T is Copy or only the values in one of the regions are used after this call

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

#[assure(
    valid_ptr(src, r),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    valid_ptr(dst, w),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`src` is valid for `count * size_of::<T>()` bytes",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`dst` is valid for `count * size_of::<T>()` bytes",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    proper_align(src),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    proper_align(dst),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`T` is `Copy` or only the values in one of the regions are used after this call",
    reason = "<specify the reason why you can assure this here>"
)]
copy(/* parameters omitted */);