Value-dependent failure with vec! initialization #3772
Description
I tried this code:
#[kani::proof]
fn vec_failure() {
let value: u8 = 1; /* set to zero and it passes */
let count: u16 = kani::any();
let vector: Vec<u8> = vec![value; count as usize];
}using the following command line invocation:
cargo kani
with Kani version:
$ cargo kani --version
cargo-kani 0.56.0
$ kani --version
kani 0.56.0
When it is run with value = 1, it produces the following failure:
Check 168: std::intrinsics::write_bytes::<u8>.precondition_instance.1
- Status: FAILURE
- Description: "memset destination region writeable"
- Location: ../../../runner/.rustup/toolchains/nightly-2024-10-03-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/intrinsics.rs:3496:9 in function std::intrinsics::write_bytes::<u8>
But when run with value = 0, it succeeds.
I expected uniform behavior in both cases, but perhaps the intrinsics special-case zero somehow?