In the following program we read from uninitialized memory so the program is undefined [0]. Using CBMC as our symbolic engine means Kani does not warn of this error. Instead the value of v[0] is symbolic/nondet. Adding a "poison" value for freshly allocated objects is likely to be a large change for CBMC. For now, we can document this behavior.

fn main() {
    let mut v: Vec<u8> = Vec::with_capacity(8);
    unsafe {
        v.set_len(3);
    }
    let _b = v[0]; //< reading uninitialized memory
}

[0] https://doc.rust-lang.org/reference/behavior-considered-undefined.html#behavior-considered-undefined

Uninitialized memory is also implicitly invalid for any type that has a restricted set of valid values. In other words, the only cases in which reading uninitialized memory is permitted are inside unions and in “padding” (the gaps between the fields/elements of a type).