From b77937e68c79f1bb19f6458f72febd5f1e9b8c72 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 19 Jun 2023 17:16:15 +0000
Subject: [PATCH] Print failed checks for global conditions

---
 kani-driver/src/call_cbmc.rs              | 12 ++++++++++++
 kani-driver/src/cbmc_property_renderer.rs | 12 +++++++++---
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 1f0debfd0c9f..3aa3ab0e8c3b 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -88,6 +88,18 @@ impl GlobalCondition {
             },
         }
     }
+
+    pub fn blame_properties<'a>(&self, properties: &'a[Property]) -> Vec<&'a Property> {
+        match &self {
+            Self::ShouldPanic { status, .. } => match *status {
+                FailedProperties::None => properties.iter().filter(|prop| prop.property_class() == "assertion" && prop.status != CheckStatus::Failure).collect(),
+                FailedProperties::Other => properties.iter().filter(|prop| prop.property_class() != "assertion" && prop.status == CheckStatus::Failure).collect(),
+                _ => vec![],
+            },
+            Self::FailUncoverable { .. } =>
+                properties.iter().filter(|prop| prop.property_class() == "cover" && prop.status != CheckStatus::Satisfied).collect(),
+            }
+    }
 }
 
 /// Our (kani-driver) notions of CBMC results.
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index fa3eb66b8bf6..486592ff9400 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -332,11 +332,11 @@ pub fn format_result(
         result_str.push_str("GLOBAL CONDITIONS:\n");
         for cond in global_conditions {
             if cond.enabled() {
-                let cond_status = if cond.passed() {
-                    CheckStatus::Success
+                let (cond_status, blame_properties) = if cond.passed() {
+                    (CheckStatus::Success, None)
                 } else {
                     global_condition_failures = true;
-                    CheckStatus::Failure
+                    (CheckStatus::Failure, Some(cond.blame_properties(&properties)))
                 };
                 result_str.push_str(&format!(
                     " - {}: {} ({})\n",
@@ -344,6 +344,12 @@ pub fn format_result(
                     cond_status,
                     cond.reason()
                 ));
+                if !cond.passed() {
+                    for prop in blame_properties.unwrap() {
+                        let failure_message = build_failure_message(prop.description.clone(), &prop.trace.clone());
+                        result_str.push_str(&failure_message);
+                    }
+                }
             }
         }
     }