kani
kani copied to clipboard
Implement checks for unchecked_* operations
Requested feature: RMC should detect failures when dealing with unchecked arithmetic operations. Use case: Unchecked arithmetic operations assume that the operands respect some invariant. If they don't, the result has an undefined behavior. We should add checks to verify that all the invariants are respected. Link to relevant documentation (Rust reference, Nomicon, RFC): https://doc.rust-lang.org/std/primitive.u32.html https://doc.rust-lang.org/std/primitive.i32.html https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked
Is this a breaking change? No
Removing soundness since we don't claim support to all UBs related to arithmetic operations.