Function pre::core::ptr::replace

pub unsafe fn replace<T>(dst: *mut T, src: T) -> T

core::ptr::replace with preconditions.

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

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

This function has preconditions

This function has the following preconditions generated by pre attributes:

• the pointer dst must be valid for reads and writes
• the pointer dst must have a proper alignment for its type
• dst points to a properly initialized value of type T

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

#[assure(
    valid_ptr(dst, r+w),
    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(
    "`dst` points to a properly initialized value of type `T`",
    reason = "<specify the reason why you can assure this here>"
)]
replace(/* parameters omitted */);