Function pre::std::ptr::drop_in_place

pub unsafe fn drop_in_place<T: ?Sized>(to_drop: *mut T)

std::ptr::drop_in_place with preconditions.

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

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

This function has preconditions

This function has the following preconditions generated by pre attributes:

• the pointer to_drop must be valid for reads and writes
• the pointer to_drop must have a proper alignment for its type
• to_drop points to a value that is valid for dropping
• T is Copy or the value at *to_drop isn't used after this call

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

#[assure(
    valid_ptr(to_drop, r+w),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    proper_align(to_drop),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`to_drop` points to a value that is valid for dropping",
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "`T` is `Copy` or the value at `*to_drop` isn\'t used after this call",
    reason = "<specify the reason why you can assure this here>"
)]
drop_in_place(/* parameters omitted */);