Spurious capacity overflow with CBMC 5.71 #1946
Description
This test is derived from https://github.com/model-checking/kani/blob/main/tests/kani/Refs/main.rs
I tried this code:
use std::collections::BTreeMap;
#[kani::proof]
#[kani::unwind(2)]
fn main() {
let arguments: BTreeMap<(), ()> = BTreeMap::new();
let _ = arguments.values().collect::<Vec<_>>()
.into_iter()
.map(|_| 5)
.collect::<Vec<_>>();
}using the following command line invocation:
kani btreemap.rs
with Kani version: bb268b1 and CBMC 5.71.0
I expected to see this happen: Verification successful
Instead, this happened: a capacity overflow check fails:
SUMMARY:
** 1 of 1148 failed (15 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
File: "/home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec.rs", line 518, in alloc::raw_vec::capacity_overflow
VERIFICATION:- FAILED
Verification Time: 3.296982s
With CBMC 5.70.0, this test passes:
SUMMARY:
** 0 of 1151 failed (20 unreachable)
VERIFICATION:- SUCCESSFUL
Verification Time: 44.638622s