Adapt to work with coverage

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)
  };

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);
 

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)