From b5b8447e7f4be7eba69d9515cce7f2fa2b200b17 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Wed, 3 Jan 2024 16:45:00 +0000
Subject: [PATCH] Adapt to work with coverage

---
 kani-driver/src/call_cbmc.rs              | 2 +-
 kani-driver/src/cbmc_property_renderer.rs | 5 ++---
 kani-driver/src/harness_runner.rs         | 8 +-------
 3 files changed, 4 insertions(+), 11 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index fc444e845d4b..f11174c18b22 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -400,7 +400,7 @@ impl VerificationResult {
                 let global_conditions = &self.global_conditions;
                 let show_checks = matches!(output_format, OutputFormat::Regular);
                 let mut result = if coverage_mode {
-                    format_coverage(results, status, failed_properties, show_checks)
+                    format_coverage(results, status, global_conditions, show_checks)
                 } else {
                     format_result(results, status, global_conditions, show_checks)
                 };
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index ac071ce65590..71d1d50d44bb 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -463,15 +463,14 @@ pub fn format_result(
 pub fn format_coverage(
     properties: &[Property],
     status: VerificationStatus,
-    should_panic: bool,
-    failed_properties: FailedProperties,
+    global_conditions: &Vec<GlobalCondition>,
     show_checks: bool,
 ) -> String {
     let (coverage_checks, non_coverage_checks): (Vec<Property>, Vec<Property>) =
         properties.iter().cloned().partition(|x| x.property_class() == "code_coverage");
 
     let verification_output =
-        format_result(&non_coverage_checks, status, should_panic, failed_properties, show_checks);
+        format_result(&non_coverage_checks, status, global_conditions, show_checks);
     let coverage_output = format_result_coverage(&coverage_checks);
     let result = format!("{}\n{}", verification_output, coverage_output);
 
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index a7987c292e54..51202faa4250 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -122,13 +122,7 @@ impl KaniSession {
             // When quiet, we don't want to print anything at all.
             // When output is old, we also don't have real results to print.
             if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
-                println!(
-                    "{}",
-                    result.render(
-                        &self.args.output_format,
-                        self.args.coverage
-                    )
-                );
+                println!("{}", result.render(&self.args.output_format, self.args.coverage));
             }
             self.gen_and_add_concrete_playback(harness, &mut result)?;
             Ok(result)