Kani should detect Rust specific undefined behavior

[celinval]

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