Treat lack of proof harnesses as success (rust-lang#1886)

Author: tedinski

kani-driver/src/harness_runner.rs

@@ -135,18 +135,27 @@ impl KaniSession {
             )
         }
 
-        if !self.args.quiet && !self.args.visualize && total > 1 {
+        // We currently omit a summary if there was just 1 harness
+        if !self.args.quiet && !self.args.visualize && total != 1 {
             if failing > 0 {
                 println!("Summary:");
             }
             for failure in failures.iter() {
                 println!("Verification failed for - {}", failure.harness.pretty_name);
             }
 
-            println!(
-                "Complete - {} successfully verified harnesses, {} failures, {} total.",
-                succeeding, failing, total
-            );
+            if total > 0 {
+                println!(
+                    "Complete - {} successfully verified harnesses, {} failures, {} total.",
+                    succeeding, failing, total
+                );
+            } else {
+                // TODO: This could use a better error message, possibly with links to Kani documentation.
+                // New users may encounter this and could use a pointer to how to write proof harnesses.
+                println!(
+                    "No proof harnesses (functions with #[kani::proof]) were found to verify."
+                );
+            }
         }
 
         #[cfg(feature = "unsound_experiments")]

kani-driver/src/metadata.rs

@@ -153,13 +153,7 @@ impl KaniSession {
             let harness = find_proof_harness(name, &metadata.proof_harnesses)?;
             return Ok(vec![harness.clone()]);
         }
-        if metadata.proof_harnesses.is_empty() {
-            // TODO: This could use a better error message, possibly with links to Kani documentation.
-            // New users may encounter this and could use a pointer to how to write proof harnesses.
-            bail!("No proof harnesses (functions with #[kani::proof]) were found to verify.");
-        } else {
-            Ok(metadata.proof_harnesses.clone())
-        }
+        Ok(metadata.proof_harnesses.clone())
     }
 }
 

tests/cargo-kani/zero-harnesses-is-success/Cargo.toml

@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "zero-harnesses-is-success"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tests/cargo-kani/zero-harnesses-is-success/expected

@@ -0,0 +1 @@
+No proof harnesses (functions with #[kani::proof]) were found to verify.

tests/cargo-kani/zero-harnesses-is-success/src/lib.rs

@@ -0,0 +1,3 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub fn nop() {}

tools/compiletest/src/runtest.rs

@@ -317,6 +317,9 @@ impl<'test> TestCx<'test> {
         let proc_res = self.compose_and_run(cargo);
         let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap();
         self.verify_output(&proc_res, &expected);
+
+        // TODO: We should probably be checking the exit status somehow
+        // See https://github.com/model-checking/kani/issues/1895
     }
 
     /// Common method used to run Kani on a single file test.