Function pre::std::ptr::write_bytes

pub unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize)

std::ptr::write_bytes with preconditions.

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

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

This function has preconditions

This function has the following preconditions generated by pre attributes:

• the pointer dst must be valid for writes
• dst is valid for count * size_of::<T>() bytes
• the pointer dst must have a proper alignment for its type
• a valid value of T is written to *dst or *dst is never used

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

#[assure(
    valid_ptr(dst, w),
    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(dst),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "a valid value of `T` is written to `*dst` or `*dst` is never used",
    reason = "<specify the reason why you can assure this here>"
)]
write_bytes(/* parameters omitted */);