Format

model-checking · Jun 20, 2023 · ed5d4ef · ed5d4ef
1 parent b77937e
commit ed5d4ef
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 7 deletions.
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -89,16 +89,30 @@ impl GlobalCondition {
  }
  }
 
- pub fn blame_properties<'a>(&self, properties: &'a[Property]) -> Vec<&'a Property> {
+ 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(),
+ 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(),
- }
+ Self::FailUncoverable { .. } => properties
+ .iter()
+ .filter(|prop| {
+ prop.property_class() == "cover" && prop.status != CheckStatus::Satisfied
+ })
+ .collect(),
+ }
  }
 }
 

diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
@@ -346,7 +346,8 @@ pub fn format_result(
  ));
  if !cond.passed() {
  for prop in blame_properties.unwrap() {
- let failure_message = build_failure_message(prop.description.clone(), &prop.trace.clone());
+ let failure_message =
+ build_failure_message(prop.description.clone(), &prop.trace.clone());
  result_str.push_str(&failure_message);
  }
  }