Valid value checks does not check char surrogate values #3241
Description
I tried this code:
#[kani::proof]
fn transmute_surrogate_ub() {
unsafe {
let val: u32 = kani::any();
kani::assume(val < char::MAX.into());
let c: char = std::mem::transmute::<u32, char>(val) as char;
match val {
0..0xD800 | 0xE000..0x110000 => assert!(char::from_u32(val).is_some()),
_ => unreachable!(),
}
}
}using the following command line invocation:
kani -Zvalid-value-checks char.rs
with Kani version: 0.52.0
I expected to see this happen: A valid value check failure
Instead, this happened: An unreachable block being reached due to UB
Failed Checks: internal error: entered unreachable code:
File: "char.rs", line 31, in transmute_surrogate_ub
VERIFICATION:- FAILED
Verification Time: 0.12348909s