Use verbosity 9 by default

model-checking · Jul 31, 2024 · f878fd9 · f878fd9
1 parent 2de6464
commit f878fd9
Show file tree

Hide file tree

Showing 9 changed files with 13 additions and 12 deletions.
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -153,6 +153,11 @@ impl KaniSession {
 
  args.push(file.to_owned().into_os_string());
 
+ // Make CBMC verbose by default to tell users about unwinding progress. This should be
+ // reviewed as CBMC's verbosity defaults evolve.
+ args.push("--verbosity".into());
+ args.push("9".into());
+
  Ok(args)
  }
 

diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh
@@ -27,8 +27,7 @@ done
 suite="perf"
 mode="cargo-kani-test"
 echo "Check compiletest suite=$suite mode=$mode"
-cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast \
- --kani-flag="--enable-unstable" --kani-flag="--cbmc-args" --kani-flag="--verbosity" --kani-flag="9"
+cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast
 exit_code=$?
 
 echo "Cleaning up..."

diff --git a/tests/cargo-kani/simple-kissat/Cargo.toml b/tests/cargo-kani/simple-kissat/Cargo.toml
@@ -12,4 +12,4 @@ description = "Tests that Kani can be invoked with Kissat"
 
 [kani.flags]
 enable-unstable = true
-cbmc-args = ["--external-sat-solver", "kissat", "--verbosity", "9" ]
+cbmc-args = ["--external-sat-solver", "kissat" ]
diff --git a/tests/ui/solver-attribute/cadical/test.rs b/tests/ui/solver-attribute/cadical/test.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that `cadical` is a valid argument to `kani::solver`
 

diff --git a/tests/ui/solver-option/bin/test.rs b/tests/ui/solver-option/bin/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver bin=kissat --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver bin=kissat
 
 //! Checks that `--solver` accepts `bin=<binary>`
 

diff --git a/tests/ui/solver-option/cadical/test.rs b/tests/ui/solver-option/cadical/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver cadical --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver cadical
 
 //! Checks that the `cadical` is supported as an argument to `--solver`
 

diff --git a/tests/ui/solver-option/kissat/test.rs b/tests/ui/solver-option/kissat/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver kissat --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver kissat
 
 //! Checks that the solver option overrides the solver attribute
 

diff --git a/tests/ui/solver-option/minisat/test.rs b/tests/ui/solver-option/minisat/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver minisat --enable-unstable --cbmc-args --verbosity 9
+// kani-flags: --solver minisat
 
 //! Checks that `--solver minisat` is accepted
 

diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py
@@ -56,8 +56,7 @@ def test_kani_perf_fail(self):
  cmd = (
  "rm -rf build target &&"
  "mkdir -p build/tests/perf/Unwind-Attribute/expected &&"
- "kani tests/kani/Unwind-Attribute/fixme_lib.rs "
- "--enable-unstable --cbmc-args --verbosity 9 > "
+ "kani tests/kani/Unwind-Attribute/fixme_lib.rs > "
  "build/tests/perf/Unwind-Attribute/expected/expected.out"
  )
  self._run_kani_perf_test(cmd, False)
@@ -66,8 +65,7 @@ def test_kani_perf_success(self):
  cmd = (
  "rm -rf build target &&"
  "mkdir -p build/tests/perf/Arbitrary/expected &&"
- "kani tests/kani/Arbitrary/arbitrary_impls.rs "
- "--enable-unstable --cbmc-args --verbosity 9 > "
+ "kani tests/kani/Arbitrary/arbitrary_impls.rs > "
  "build/tests/perf/Arbitrary/expected/expected.out"
  )
  self._run_kani_perf_test(cmd, True)