Bump CBMC version (#2067)

Author: zhassan-aws

kani-dependencies

@@ -1,3 +1,3 @@
-CBMC_VERSION="5.72.0"
+CBMC_VERSION="5.75.0"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.8"

scripts/kani-regression.sh

@@ -22,7 +22,7 @@ KANI_DIR=$SCRIPT_DIR/..
 export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
 
 # Required dependencies
-check-cbmc-version.py --major 5 --minor 72
+check-cbmc-version.py --major 5 --minor 75
 check-cbmc-viewer-version.py --major 3 --minor 5
 
 # Formatting check

tests/cargo-kani/itoa_dep/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "itoa_dep"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+itoa = "1.0.5"

tests/cargo-kani/itoa_dep/check_signed.expected

@@ -0,0 +1,7 @@
+Status: SUCCESS\
+Description: "assertion failed: result == &output"
+
+Status: FAILURE\
+Description: "memcpy source region readable"
+
+VERIFICATION:- FAILED

tests/cargo-kani/itoa_dep/src/main.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks Kani's support for the `itoa` crate
+//! Currently fails with a spurious failure:
+//! https://github.com/model-checking/kani/issues/2066
+
+use itoa::{Buffer, Integer};
+use std::fmt::Write;
+
+fn check_itoa<T: kani::Arbitrary + Integer + std::fmt::Display>() {
+    let input: T = kani::any();
+    let mut buf = Buffer::new();
+    let result = buf.format(input);
+    let mut output = String::new();
+    write!(&mut output, "{}", input);
+    assert_eq!(result, &output);
+}
+
+#[kani::proof]
+#[kani::unwind(10)]
+fn check_signed() {
+    check_itoa::<i8>();
+}
+
+fn main() {}