Print failed checks for global conditions

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.

kani-driver/src/cbmc_property_renderer.rs

@@ -332,18 +332,24 @@ 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",
  cond.name(),
  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);
+ }
+ }
  }
  }
  }