Added test + fix small formatting with harness runner

kani-driver/src/harness_runner.rs

@@ -4,22 +4,19 @@
 use anyhow::{bail, Result};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
+use std::fs::File;
+use std::io::Write;
 use std::path::Path;
-use std::thread;
 use std::sync::mpsc;
 use std::sync::Arc;
+use std::thread;
 use std::time::Instant;
-use std::fs::File;
-use std::io::Write;
 
 use crate::args::OutputFormat;
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
 use crate::session::KaniSession;
 
-use std::fs::File;
-use std::io::Write;
-
 use std::env::current_dir;
 use std::path::PathBuf;
 
@@ -34,7 +31,6 @@ pub(crate) struct HarnessRunner<'sess, 'pr> {
     pub project: &'pr Project,
 }
 
-
 /// The result of checking a single harness. This both hangs on to the harness metadata
 /// (as a means to identify which harness), and provides that harness's verification result.
 pub(crate) struct HarnessResult<'pr> {
@@ -52,7 +48,7 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
         self.check_stubbing(harnesses)?;
 
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
-        let max_threads = 8; 
+        let max_threads = 8;
         let pool = {
             let mut builder = rayon::ThreadPoolBuilder::new();
             let mut threads = sorted_harnesses.len();
@@ -62,7 +58,7 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
             builder = builder.num_threads(threads);
             builder.build()?
         };
-        
+
         let before = Instant::now();
 
         let results = pool.install(|| -> Result<Vec<HarnessResult<'pr>>> {
@@ -73,13 +69,13 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
                     let report_dir = self.project.outdir.join(format!("report-{harness_filename}"));
                     let goto_file =
                         self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap();
-                
+
                     self.sess.instrument_model(goto_file, goto_file, &self.project, &harness)?;
 
                     if self.sess.args.synthesize_loop_contracts {
                         self.sess.synthesize_loop_contracts(goto_file, &goto_file, &harness)?;
                     }
-                    
+
                     let result = self.sess.check_harness(goto_file, &report_dir, harness)?;
                     Ok(HarnessResult { harness, result })
                 })
@@ -119,19 +115,14 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
     }
 }
 
-
 impl KaniSession {
     fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) {
         if self.should_print_output() {
             if self.args.output_into_files {
                 self.write_output_to_file(result, harness);
             }
 
-            let output = result.render(
-                &self.args.output_format,
-                harness.attributes.should_panic,
-                self.args.coverage,
-            );
+            let output = result.render(&self.args.output_format, harness.attributes.should_panic);
             println!("{}", output);
         }
     }
@@ -148,11 +139,7 @@ impl KaniSession {
 
         std::fs::create_dir_all(prefix).unwrap();
         let mut file = File::create(&file_name).unwrap();
-        let file_output = result.render(
-            &OutputFormat::Regular,
-            harness.attributes.should_panic,
-            self.args.coverage,
-        );
+        let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic);
 
         if let Err(e) = writeln!(file, "{}", file_output) {
             eprintln!(

tests/script-based-pre/individual_file_output/config.yml

@@ -0,0 +1,3 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: individual_file_output.sh

tests/script-based-pre/individual_file_output/individual_file_output.sh

@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+OUT_DIR=tmp_sample_crate
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+
+# Move the original source to the output folder since it will be modified
+cp -r sample_crate ${OUT_DIR}
+pushd $OUT_DIR
+
+echo "Run verification..."
+../../../../scripts/cargo-kani -Z unstable-options --output-into-files
+
+OUTPUT_DIR="kani_results" 
+
+# Check if the output directory exists
+if [ ! -d "$OUTPUT_DIR" ]; then
+    echo "Output directory $OUT_DIR/$OUTPUT_DIR does not exist. Verification failed."
+    exit 1
+fi
+
+# Check if there are any files in the output directory
+output_files=("$OUTPUT_DIR"/*)
+
+if [ ${#output_files[@]} -eq 0 ]; then
+    echo "No files found in the output directory. Verification failed."
+    exit 1
+fi
+
+# Check if each file contains text
+for file in "${output_files[@]}"; do
+    if [ ! -s "$file" ]; then
+        echo "File $file is empty. Verification failed."
+        exit 1
+    else
+        echo "File $file is present and contains text."
+    fi
+done
+
+popd
+rm -rf ${OUT_DIR}

tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "sample_crate"
+version = "0.1.0"
+edition = "2021"
+
+[package.metadata.kani.flags]
+concrete-playback = "inplace"
+
+[package.metadata.kani.unstable]
+concrete-playback = true
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that we can correctly generate tests from a cover statement and run them.
+
+#[cfg(kani)]
+mod verify {
+    #[kani::proof]
+    fn any_is_ok() {
+        let result: Result<char, bool> = kani::any();
+        kani::cover!(result.is_ok());
+    }
+
+    #[kani::proof]
+    fn any_is_err() {
+        let result: Result<char, bool> = kani::any();
+        kani::cover!(result.is_err());
+    }
+}