RMC incorrectly reports an assertion failure on a two-dimensional vector

[zhassan-aws]

I tried this code:

fn main() {
    let a: Vec<Vec<i32>> = vec![vec![0; 2]; 1];
    assert!(a.len() == 1);
}

using the following command line invocation:

rmc test.rs

with RMC version: main-154-2021-08-06

I expected the assertion to pass, but it didn't:

[main.assertion.1] line 3 assertion failed: a.len() == 1: FAILURE

If I compile the test and run it, the assertion is not hit:

$ rustc test.rs 
$ ./test 
$ 

Also, if I modify the first line in the function to

    let a: Vec<Vec<i32>> = vec![vec![0; 2]];

i.e. leave out the length for the outer vector, the assertion passes.

[chinmaydd]

The call hierarchy on using the vec! macro for initialization of a Vec with a value looks like:

• from_elem
• from_elem
• extend_with

extend_with uses the SetLenOnDrop optimization as described in #191. Since rmc does not currently handle drop behavior, the length of the Vec does not hold the correct value after initialization. This behavior should be fixed by a combination #402 and #336.

[avanhatt]

Added as a unit test in #402