[][src]Function pre::core::mut_pointer__impl__copy_from__

pub fn mut_pointer__impl__copy_from__()

A stub for the preconditions of the core::mut_pointer<T>::copy_from function.

What is this function?

This function was generated by an impl block inside a extern_crate attribute that looked like this:

This example is not tested
impl< T > mut_pointer < T > where T : ? Sized {
    unsafe fn copy_from(self, src : * const T, count : usize);
    /* other items omitted */
}

Preconditions on external functions inside of an impl block are attached to empty functions like this one. When the preconditions should be checked, a call to this function is inserted, which triggers checking the preconditions.

This function has preconditions

This function has the following preconditions generated by pre attributes:

  • the pointer src must be valid for reads
  • the pointer self must be valid for writes
  • src is valid for count * size_of::<T>() bytes
  • self is valid for count * size_of::<T>() bytes
  • the pointer src must have a proper alignment for its type
  • the pointer self 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:

This example is not tested
#[forward(impl pre::core::mut_pointer)]
#[assure(
    valid_ptr(src, r),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    valid_ptr(self, 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(
    "`self` 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(self),
    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>"
)]
x.copy_from(/* parameters omitted */);