Requested feature: Kani should implement UB checks for all behavior listed in the Rust reference, such as value validity tests, pointer aliasing rules.
Use case: Rust code that uses unsafe
Link to relevant documentation (Rust reference, Nomicon, RFC): https://doc.rust-lang.org/reference/behavior-considered-undefined.html

Related issues:

• Implement validity checks #3085
• Reading uninitialized memory gives symbolic value rather than error #920
• Object aliasing violations are not detected #314
• Tracking Issue: Automatically Verify Memory Initialization #3300