diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 3aa3ab0e8c3b..982aef8bcd66 100644 --- 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 index 486592ff9400..e255e55fbd2d 100644 --- 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); } }