kani icon indicating copy to clipboard operation
kani copied to clipboard

Implement checks for unchecked_* operations

Open celinval opened this issue 4 years ago • 1 comments

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

celinval avatar Nov 15 '21 22:11 celinval

Removing soundness since we don't claim support to all UBs related to arithmetic operations.

celinval avatar Jul 14 '22 18:07 celinval