Spurious failure when calling vec! with a size of zero

[adpaco-aws]

#79 added a new test in rust-tests/cbmc-reg/NondetVectors/fixme_main.rs where a Vector is initialized with a nondet. value, but this is not supported at the moment.

[zhassan-aws]

The spurious failure only happens when calling vec! with a length of 0 for i8 or u8. Here's a minimal reproducer:

#[kani::proof]
fn main() {
    let v: Vec<i8> = vec![kani::any(); 0];
}

This produces:

SUMMARY:
 ** 1 of 112 failed (5 unreachable)
Failed Checks: memset destination region writeable
 File: "/home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/intrinsics.rs", line 2590, in std::intrinsics::write_bytes::<i8>

VERIFICATION:- FAILED

If I change i8 to i16/u16 or i32/u32, the failure disappears. For example, this is the result with i16:

SUMMARY:
 ** 0 of 349 failed (8 unreachable)

VERIFICATION:- SUCCESSFUL

[zhassan-aws]

Actually, I get the spurious failure even without using kani::any() at all:

#[kani::proof]
fn main() {
    let v: Vec<i8> = vec![5; 0];
}

I suspect this might be to the dangling pointer issue that we've seen previously with vectors of size 0.

[tautschnig]

codegen_write_bytes needs to make a count of 0 a special case and not invoke memset, just like we already do for calls of memcmp.