diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 9191e8250550..4ce5be4bed8b 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -89,3 +89,8 @@ jobs: - name: Execute Kani performance tests working-directory: ./kani run: ./scripts/kani-perf.sh + + - name: Execute Kani performance ignored tests + working-directory: ./kani + continue-on-error: true + run: cargo run -p compiletest -- --suite perf --mode cargo-kani-test ignore --ignored diff --git a/tests/perf/btreeset/insert_same/Cargo.toml b/tests/perf/btreeset/ignore_insert_same/Cargo.toml similarity index 100% rename from tests/perf/btreeset/insert_same/Cargo.toml rename to tests/perf/btreeset/ignore_insert_same/Cargo.toml diff --git a/tests/perf/btreeset/insert_same/expected b/tests/perf/btreeset/ignore_insert_same/expected similarity index 100% rename from tests/perf/btreeset/insert_same/expected rename to tests/perf/btreeset/ignore_insert_same/expected diff --git a/tests/perf/btreeset/insert_same/src/main.rs b/tests/perf/btreeset/ignore_insert_same/src/main.rs similarity index 100% rename from tests/perf/btreeset/insert_same/src/main.rs rename to tests/perf/btreeset/ignore_insert_same/src/main.rs diff --git a/tests/perf/vec/string/Cargo.toml b/tests/perf/vec/ignore_string/Cargo.toml similarity index 100% rename from tests/perf/vec/string/Cargo.toml rename to tests/perf/vec/ignore_string/Cargo.toml diff --git a/tests/perf/vec/box_dyn/Cargo.toml b/tests/perf/vec/ignore_string/box_dyn/Cargo.toml similarity index 100% rename from tests/perf/vec/box_dyn/Cargo.toml rename to tests/perf/vec/ignore_string/box_dyn/Cargo.toml diff --git a/tests/perf/vec/box_dyn/expected b/tests/perf/vec/ignore_string/box_dyn/expected similarity index 100% rename from tests/perf/vec/box_dyn/expected rename to tests/perf/vec/ignore_string/box_dyn/expected diff --git a/tests/perf/vec/box_dyn/src/main.rs b/tests/perf/vec/ignore_string/box_dyn/src/main.rs similarity index 100% rename from tests/perf/vec/box_dyn/src/main.rs rename to tests/perf/vec/ignore_string/box_dyn/src/main.rs diff --git a/tests/perf/vec/string/expected b/tests/perf/vec/ignore_string/expected similarity index 100% rename from tests/perf/vec/string/expected rename to tests/perf/vec/ignore_string/expected diff --git a/tests/perf/vec/string/src/main.rs b/tests/perf/vec/ignore_string/src/main.rs similarity index 100% rename from tests/perf/vec/string/src/main.rs rename to tests/perf/vec/ignore_string/src/main.rs diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs index fc7ac84b5680..afb9057ad451 100644 --- a/tools/compiletest/src/header.rs +++ b/tools/compiletest/src/header.rs @@ -180,21 +180,17 @@ pub fn make_test_description( path: &Path, src: R, ) -> test::TestDesc { - let mut ignore = false; let mut should_fail = false; - let mut ignore_message = None; - if config.mode == Mode::Kani || config.mode == Mode::Stub { - // If the path to the test contains "fixme" or "ignore", skip it. - let file_path = path.to_str().unwrap(); - (ignore, ignore_message) = if file_path.contains("fixme") { - (true, Some("fixme test")) - } else if file_path.contains("ignore") { - (true, Some("ignore test")) - } else { - (false, None) - }; - } + // If the path to the test contains "fixme" or "ignore", skip it. + let file_path = path.to_str().unwrap(); + let (mut ignore, mut ignore_message) = if file_path.contains("fixme") { + (true, Some("fixme test")) + } else if file_path.contains("ignore") { + (true, Some("ignore test")) + } else { + (false, None) + }; // The `KaniFixme` mode runs tests that are ignored in the `kani` suite if config.mode == Mode::KaniFixme { @@ -207,8 +203,10 @@ pub fn make_test_description( // If the base name does NOT contain "fixme" or "ignore", we skip it. // All "fixme" tests are expected to fail - (ignore, ignore_message) = if base_name.contains("fixme") || base_name.contains("ignore") { + (ignore, ignore_message) = if base_name.contains("fixme") { (false, None) + } else if base_name.contains("ignore") { + (true, Some("ignore test")) } else { (true, Some("regular test")) };