diff --git a/tests/cargo-kani/itoa_dep/src/main.rs b/tests/cargo-kani/itoa_dep/src/main.rs index 9bda87de7339..ea729e7c1c20 100644 --- a/tests/cargo-kani/itoa_dep/src/main.rs +++ b/tests/cargo-kani/itoa_dep/src/main.rs @@ -20,7 +20,7 @@ fn check_itoa() { #[kani::proof] #[kani::unwind(10)] fn check_signed() { - check_itoa::(); + check_itoa::(); } fn main() {} diff --git a/tests/perf/format/Cargo.toml b/tests/perf/format/Cargo.toml new file mode 100644 index 000000000000..3fe392e07c04 --- /dev/null +++ b/tests/perf/format/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "format" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/perf/format/expected b/tests/perf/format/expected new file mode 100644 index 000000000000..44572d1c72bf --- /dev/null +++ b/tests/perf/format/expected @@ -0,0 +1 @@ +Complete - 2 successfully verified harnesses, 0 failures, 2 total diff --git a/tests/perf/format/src/lib.rs b/tests/perf/format/src/lib.rs new file mode 100644 index 000000000000..ad14c6288e7c --- /dev/null +++ b/tests/perf/format/src/lib.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance of calling format. +//! This tests capture the performance regression introduced by the toolchain upgrade #2551. +//! See https://github.com/model-checking/kani/issues/2576 for more details. + +#[kani::proof] +fn fmt_i8() { + let num: i8 = kani::any(); + let s = format!("{num}"); + assert!(s.len() <= 4); +} + +#[kani::proof] +fn fmt_u8() { + let num: u8 = kani::any(); + let s = format!("{num}"); + assert!(s.len() <= 3); +}