Uninitialized memory detection mitigates delayed UB, but does not support it fully #3324
Description
I tried this code:
#[kani::proof]
fn invalid_value() {
unsafe {
let mut value: u128 = 0;
let ptr = &mut value as *mut _ as *mut (u8, u32, u64);
*ptr = (4, 4, 4); // This assignment itself does not cause UB...
assert!(value > 0); // ...but this reads a padding value! ⚠️
}
}using the following command line invocation:
kani -Z ghost-state -Z uninit-checks delayed-ub.rs
with Kani version: 0.53
I expected to see this happen: Verification should fail since we are reading padding values.
Instead, this happened: Verification succeed