Requested feature: Kani should automatically check if unsafe operations can break validity invariants which can trigger UB. According to the Rust reference, producing an invalid value, even in private fields and locals is undefined behavior. "Producing" a value happens any time a value is assigned to or read from a place, passed to a function/primitive operation or returned from a function/primitive operation.
Use case: Checking that unsafe code doesn't trigger UB.
Link to relevant documentation (Rust reference, Nomicon, RFC): Rust UB reference and definition of validity invariant.

Test case:

#[kani::requires(!ptr.is_null())]
#[kani::ensures(!result.as_ptr().is_null())] // Compiler warns that this should always be nonnull().
pub unsafe fn new_unchecked<T>(ptr: *mut T) -> NonNull<T> {
    NonNull::<T>::new_unchecked(ptr)
}

Since it is not possible to programmatically verify undefined behavior, Kani compiler must insert checks before the UB actually happens.

Tasks

• RFC for UB checks
• Implement basic checks
• Mitigate checks that aren't implemented yet
• Add tests