Function pre::core::ptr::read[][src]

pub unsafe fn read<T>(src: *const T) -> T
Expand description

core::ptr::read with preconditions.

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

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

This function has preconditions

This function has the following preconditions generated by pre attributes:

  • the pointer src must be valid for reads
  • the pointer src must have a proper alignment for its type
  • src points to a properly initialized value of type T
  • T is Copy or the value at *src isn’t 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(
    proper_align(src),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`src` points to a properly initialized value of type `T`",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`T` is `Copy` or the value at `*src` isn't used after this call",
    reason = "<specify the reason why you can assure this here>"
)]
read(/* parameters omitted */);