fix formatting & regression failures

model-checking · Feb 4, 2025 · bfebfdb · bfebfdb
1 parent eaab5cf
commit bfebfdb
Show file tree

Hide file tree

Showing 10 changed files with 43 additions and 22 deletions.
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -104,8 +104,8 @@ impl CodegenUnits {
                 // and these harnesses have no stubs.
                 units.extend(
                     automatic_harnesses
-                        .iter()
-                        .map(|(harness, _)| CodegenUnit {
+                        .keys()
+                        .map(|harness| CodegenUnit {
                             harnesses: vec![*harness],
                             stubs: HashMap::default(),
                         })

diff --git a/kani-driver/src/args/autoverify_args.rs b/kani-driver/src/args/autoverify_args.rs
@@ -71,7 +71,7 @@ impl ValidateArgs for CargoAutoverifyArgs {
                 ErrorKind::MissingRequiredArgument,
                 format!(
                     "The `autoverify` subcommand is unstable and requires -Z {}",
-                    UnstableFeature::UnstableOptions.to_string()
+                    UnstableFeature::UnstableOptions
                 ),
             ));
         }
@@ -105,7 +105,7 @@ impl ValidateArgs for StandaloneAutoverifyArgs {
                 ErrorKind::MissingRequiredArgument,
                 format!(
                     "The `autoverify` subcommand is unstable and requires -Z {}",
-                    UnstableFeature::UnstableOptions.to_string()
+                    UnstableFeature::UnstableOptions
                 ),
             ));
         }

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
@@ -167,29 +167,31 @@ impl KaniSession {
         harness: &HarnessMetadata,
     ) -> Result<VerificationResult> {
         let thread_index = rayon::current_thread_index().unwrap_or_default();
-        // If the harness is automatically generated, pretty_name refers to the function under verification.
-        let mut msg = if harness.is_automatically_generated {
-            if matches!(harness.attributes.kind, HarnessKind::Proof) {
-                format!(
-                    "Autoverify: Checking function {} against all possible inputs...",
-                    harness.pretty_name
-                )
+        if !self.args.common_args.quiet {
+            // If the harness is automatically generated, pretty_name refers to the function under verification.
+            let mut msg = if harness.is_automatically_generated {
+                if matches!(harness.attributes.kind, HarnessKind::Proof) {
+                    format!(
+                        "Autoverify: Checking function {} against all possible inputs...",
+                        harness.pretty_name
+                    )
+                } else {
+                    format!(
+                        "Autoverify: Checking function {}'s contract against all possible inputs...",
+                        harness.pretty_name
+                    )
+                }
             } else {
-                format!(
-                    "Autoverify: Checking function {}'s contract against all possible inputs...",
-                    harness.pretty_name
-                )
+                format!("Checking harness {}...", harness.pretty_name)
+            };
+
+            if rayon::current_num_threads() > 1 {
+                msg = format!("Thread {thread_index}: {msg}");
             }
-        } else {
-            format!("Checking harness {}...", harness.pretty_name)
-        };
 
-        if rayon::current_num_threads() > 1 {
-            msg = format!("Thread {thread_index}: {msg}");
+            println!("{msg}");
         }
 
-        println!("{msg}");
-
         let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
         self.process_output(&result, harness, thread_index);

diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
@@ -228,6 +228,7 @@ pub mod tests {
             goto_file: model_file,
             contract: Default::default(),
             has_loop_contracts: false,
+            is_automatically_generated: false,
         }
     }
 

diff --git a/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml b/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "cargo_autoverify_contracts"
 version = "0.1.0"

diff --git a/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml b/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "cargo_autoverify_include"
 version = "0.1.0"

diff --git a/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml b/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "cargo_autoverify_filter"
 version = "0.1.0"

diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml b/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "cargo_autoverify_harnesses_fail"
 version = "0.1.0"

diff --git a/tests/script-based-pre/cargo_autoverify_include/Cargo.toml b/tests/script-based-pre/cargo_autoverify_include/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "cargo_autoverify_include"
 version = "0.1.0"

diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "cargo_autoverify_loops_fixme"
 version = "0.1.0"