float to int saturating cast #4536
Description
$ rustc --version
rustc 1.91.0-nightly (02c7b1a7a 2025-09-13)According to the Rust docs:
Since Rust 1.45, the
askeyword performs a saturating cast when casting from float to int. If the floating point value exceeds the upper bound or is less than the lower bound, the returned value will be equal to the bound crossed.
We can check this with the following program
fn main() {
let x: f32 = 300.0;
let y: u8 = x as u8;
println!("{}", y);
}$ rustc main.rs && ./main
255But Kani seems to disagree:
#[cfg(kani)]
#[kani::proof]
fn check_float_to_int() {
let x: f32 = 300.0;
let y: u8 = x as u8;
assert!(y == 255);
}$ kani main.rs --harness check_float_to_int
...
RESULTS:
Check 1: check_float_to_int.assertion.1
- Status: FAILURE
- Description: "assertion failed: y == 255"
- Location: main.rs:12:5 in function check_float_to_int
SUMMARY:
** 1 of 1 failed
Failed Checks: assertion failed: y == 255
File: "main.rs", line 12, in check_float_to_int
VERIFICATION:- FAILEDChanging the assert to y == 44 (300 % 256):
#[cfg(kani)]
#[kani::proof]
fn check_float_to_int() {
let x: f32 = 300.0;
let y: u8 = x as u8;
assert!(y == 44);
}$ kani main.rs --harness check_float_to_int
...
RESULTS:
Check 1: check_float_to_int.assertion.1
- Status: SUCCESS
- Description: "assertion failed: y == 44"
- Location: main.rs:12:5 in function check_float_to_int
SUMMARY:
** 0 of 1 failed
VERIFICATION:- SUCCESSFUL