Update status to COVERED, UNCOVERED

kani-driver/src/cbmc_output_parser.rs

@@ -96,16 +96,19 @@ pub struct PropertyId {
 
 impl Property {
     const COVER_PROPERTY_CLASS: &str = "cover";
-    const COVERAGE_PROPERTY_CLASS: &str = "coverage";
+    const COVERAGE_PROPERTY_CLASS: &str = "code_coverage";
 
     pub fn property_class(&self) -> String {
         self.property_id.class.clone()
     }
 
+    pub fn is_code_coverage_property(&self) -> bool {
+        self.property_id.class == Self::COVERAGE_PROPERTY_CLASS
+    }
+
     /// Returns true if this is a cover property
     pub fn is_cover_property(&self) -> bool {
-        self.property_id.class == Self::COVERAGE_PROPERTY_CLASS
-            || self.property_id.class == Self::COVER_PROPERTY_CLASS
+        self.property_id.class == Self::COVER_PROPERTY_CLASS
     }
 
     pub fn property_name(&self) -> String {
@@ -324,10 +327,12 @@ impl std::fmt::Display for TraceData {
 #[serde(rename_all = "UPPERCASE")]
 pub enum CheckStatus {
     Failure,
+    Covered,   // for code coverage
     Satisfied, // for cover properties only
     Success,
     Undetermined,
     Unreachable,
+    Uncovered,     // for code coverage
     Unsatisfiable, // for cover properties only
 }
 
@@ -336,6 +341,8 @@ impl std::fmt::Display for CheckStatus {
         let check_str = match self {
             CheckStatus::Satisfied => style("SATISFIED").green(),
             CheckStatus::Success => style("SUCCESS").green(),
+            CheckStatus::Covered => style("COVERED").green(),
+            CheckStatus::Uncovered => style("UNCOVERED").yellow(),
             CheckStatus::Failure => style("FAILURE").red(),
             CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
             CheckStatus::Undetermined => style("UNDETERMINED").yellow(),

kani-driver/src/cbmc_property_renderer.rs

@@ -464,7 +464,7 @@ fn format_result_coverage(properties: &[Property]) -> String {
         let src = prop.source_location.clone();
         let file_entries = coverage_results.entry(src.file.unwrap()).or_default();
         let check_status =
-            if prop.status == CheckStatus::Failure { CoverStatus::Full } else { CoverStatus::None };
+            if prop.status == CheckStatus::Covered { CoverStatus::Full } else { CoverStatus::None };
 
         // Create Map<file, Map<line, status>>
         file_entries
@@ -581,7 +581,8 @@ pub fn postprocess_result(properties: Vec<Property>, extra_ptr_checks: bool) ->
 
     let updated_properties =
         update_properties_with_reach_status(properties_filtered, has_fundamental_failures);
-    update_results_of_cover_checks(updated_properties)
+    let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties);
+    update_results_of_cover_checks(results_after_code_coverage)
 }
 
 /// Determines if there is property with status `FAILURE` and the given description
@@ -682,6 +683,24 @@ fn update_properties_with_reach_status(
     properties
 }
 
+/// Update the results of code coverage (NOT cover) properties.
+/// - SUCCESS -> UNCOVERED
+/// - FAILURE -> COVERED
+/// Note that these statuses are intermediate statuses that aren't reported to users but rather internally consumed
+/// and reported finally as PARTIAL, FULL or NONE based on aggregated line coverage results.
+fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Vec<Property> {
+    for prop in properties.iter_mut() {
+        if prop.is_code_coverage_property() {
+            if prop.status == CheckStatus::Success {
+                prop.status = CheckStatus::Uncovered;
+            } else if prop.status == CheckStatus::Failure {
+                prop.status = CheckStatus::Covered;
+            }
+        }
+    }
+    properties
+}
+
 /// Update the results of cover properties.
 /// We encode cover(cond) as assert(!cond), so if the assertion
 /// fails, then the cover property is satisfied and vice versa.