From 6ad6913c69f06ed2c67b3a74209bcf37e7c29813 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 5 Jun 2023 17:22:43 +0000
Subject: [PATCH 01/14] Add `--fail-uncoverable` option and rework global
 conditions

---
 kani-driver/src/args/mod.rs               |   3 +
 kani-driver/src/call_cbmc.rs              | 134 ++++++++++++++++++----
 kani-driver/src/cbmc_property_renderer.rs |  45 +++++---
 kani-driver/src/harness_runner.rs         |   5 +-
 4 files changed, 144 insertions(+), 43 deletions(-)

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index dbc80fedbb99..2b9b51e42636 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -156,6 +156,9 @@ pub struct VerificationArgs {
     #[arg(long)]
     pub force_build: bool,
 
+    #[arg(long, requires("enable_unstable"))]
+    pub fail_uncoverable: bool,
+
     /// Toggle between different styles of output
     #[arg(long, default_value = "regular", ignore_case = true, value_enum)]
     pub output_format: OutputFormat,
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index daddfdf62f1c..7de2620be2cd 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -24,7 +24,7 @@ pub enum VerificationStatus {
 
 /// Represents failed properties in three different categories.
 /// This simplifies the process to determine and format verification results.
-#[derive(Clone, Copy, Debug)]
+#[derive(Clone, Copy, Debug, PartialEq)]
 pub enum FailedProperties {
     // No failures
     None,
@@ -34,13 +34,51 @@ pub enum FailedProperties {
     Other,
 }
 
+// Represents the global status for cover statements in two categories.
+#[derive(Clone, Copy, Debug, PartialEq)]
+pub enum CoversStatus {
+    // All cover statements are satisfied
+    AllSatisfied,
+    // Not all cover statement are satisfied
+    Other,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq)]
+pub enum GlobalCondition {
+    ShouldPanic { enabled: bool, status: FailedProperties },
+    FailUncoverable { enabled: bool, status: CoversStatus },
+}
+
+impl GlobalCondition {
+    pub fn enabled(&self) -> bool {
+        match &self {
+            Self::ShouldPanic { enabled, .. } => *enabled,
+            Self::FailUncoverable { enabled, .. } => *enabled,
+        }
+    }
+
+    pub fn name(&self) -> &str {
+        match &self {
+            Self::ShouldPanic { .. } => "should_panic",
+            Self::FailUncoverable { .. } => "fail_uncoverable",
+        }
+    }
+
+    pub fn passed(&self) -> bool {
+        match &self {
+            Self::ShouldPanic { status, .. } => *status == FailedProperties::PanicsOnly,
+            Self::FailUncoverable { status, .. } => *status == CoversStatus::AllSatisfied,
+        }
+    }
+}
+
 /// Our (kani-driver) notions of CBMC results.
 #[derive(Debug)]
 pub struct VerificationResult {
     /// Whether verification should be considered to have succeeded, or have failed.
     pub status: VerificationStatus,
     /// The compact representation for failed properties
-    pub failed_properties: FailedProperties,
+    pub global_conditions: Vec<GlobalCondition>,
     /// The parsed output, message by message, of CBMC. However, the `Result` message has been
     /// removed and is available in `results` instead.
     pub messages: Option<Vec<ParserItem>>,
@@ -89,7 +127,12 @@ impl KaniSession {
                 )
             })?;
 
-            VerificationResult::from(output, harness.attributes.should_panic, start_time)
+            VerificationResult::from(
+                output,
+                harness.attributes.should_panic,
+                self.args.fail_uncoverable,
+                start_time,
+            )
         };
 
         Ok(verification_results)
@@ -249,17 +292,19 @@ impl VerificationResult {
     fn from(
         output: VerificationOutput,
         should_panic: bool,
+        fail_uncoverable: bool,
         start_time: Instant,
     ) -> VerificationResult {
         let runtime = start_time.elapsed();
         let (items, results) = extract_results(output.processed_items);
-
+        // let global_conditions: Vec<GlobalCondition> = vec![GlobalCondition::ShouldPanic { enabled: should_panic, status: None },
+        // FailUncoverable { enabled: fail_uncoverable, status: None }];
         if let Some(results) = results {
-            let (status, failed_properties) =
-                verification_outcome_from_properties(&results, should_panic);
+            let (status, global_conditions) =
+                verification_outcome_from_properties(&results, should_panic, fail_uncoverable);
             VerificationResult {
                 status,
-                failed_properties,
+                global_conditions,
                 messages: Some(items),
                 results: Ok(results),
                 runtime,
@@ -269,7 +314,7 @@ impl VerificationResult {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
             VerificationResult {
                 status: VerificationStatus::Failure,
-                failed_properties: FailedProperties::Other,
+                global_conditions: vec![],
                 messages: Some(items),
                 results: Err(output.process_status),
                 runtime,
@@ -281,7 +326,7 @@ impl VerificationResult {
     pub fn mock_success() -> VerificationResult {
         VerificationResult {
             status: VerificationStatus::Success,
-            failed_properties: FailedProperties::None,
+            global_conditions: vec![],
             messages: None,
             results: Ok(vec![]),
             runtime: Duration::from_secs(0),
@@ -292,7 +337,7 @@ impl VerificationResult {
     fn mock_failure() -> VerificationResult {
         VerificationResult {
             status: VerificationStatus::Failure,
-            failed_properties: FailedProperties::Other,
+            global_conditions: vec![],
             messages: None,
             // on failure, exit codes in theory might be used,
             // but `mock_failure` should never be used in a context where they will,
@@ -303,14 +348,13 @@ impl VerificationResult {
         }
     }
 
-    pub fn render(&self, output_format: &OutputFormat, should_panic: bool) -> String {
+    pub fn render(&self, output_format: &OutputFormat) -> String {
         match &self.results {
             Ok(results) => {
                 let status = self.status;
-                let failed_properties = self.failed_properties;
+                let global_conditions = &self.global_conditions;
                 let show_checks = matches!(output_format, OutputFormat::Regular);
-                let mut result =
-                    format_result(results, status, should_panic, failed_properties, show_checks);
+                let mut result = format_result(results, status, global_conditions, show_checks);
                 writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
                 result
             }
@@ -338,20 +382,52 @@ impl VerificationResult {
 fn verification_outcome_from_properties(
     properties: &[Property],
     should_panic: bool,
-) -> (VerificationStatus, FailedProperties) {
+    fail_uncoverable: bool,
+) -> (VerificationStatus, Vec<GlobalCondition>) {
+    let should_panic_cond = should_panic_cond(should_panic, properties);
+    let fail_uncoverable_cond = fail_uncoverable_cond(fail_uncoverable, properties);
+    // let failed_covers = determine_failed_covers(properties);
+    let global_conditions = vec![should_panic_cond, fail_uncoverable_cond];
+    // global_conditions.push();
+    let status = outcome_from_global_conditions(properties, &global_conditions);
+    (status, global_conditions)
+}
+
+fn should_panic_cond(enabled: bool, properties: &[Property]) -> GlobalCondition {
     let failed_properties = determine_failed_properties(properties);
-    let status = if should_panic {
-        match failed_properties {
-            FailedProperties::None | FailedProperties::Other => VerificationStatus::Failure,
-            FailedProperties::PanicsOnly => VerificationStatus::Success,
+    GlobalCondition::ShouldPanic { enabled, status: failed_properties }
+}
+
+fn fail_uncoverable_cond(enabled: bool, properties: &[Property]) -> GlobalCondition {
+    let failed_covers = determine_failed_covers(properties);
+    GlobalCondition::FailUncoverable { enabled, status: failed_covers }
+}
+
+fn outcome_from_global_conditions(
+    properties: &[Property],
+    global_conditions: &[GlobalCondition],
+) -> VerificationStatus {
+    let enabled_global_conditions = !global_conditions
+        .iter()
+        .filter(|cond| cond.enabled())
+        .collect::<Vec<&GlobalCondition>>()
+        .is_empty();
+    if !enabled_global_conditions {
+        let failed_properties = determine_failed_properties(properties);
+        if failed_properties == FailedProperties::None {
+            VerificationStatus::Success
+        } else {
+            VerificationStatus::Failure
         }
     } else {
-        match failed_properties {
-            FailedProperties::None => VerificationStatus::Success,
-            FailedProperties::PanicsOnly | FailedProperties::Other => VerificationStatus::Failure,
+        let all_global_conditions_passed =
+            global_conditions.iter().all(|cond| if cond.enabled() { cond.passed() } else { true });
+        if all_global_conditions_passed {
+            VerificationStatus::Success
+        } else {
+            VerificationStatus::Failure
         }
-    };
-    (status, failed_properties)
+    }
 }
 
 /// Determines the `FailedProperties` variant that corresponds to an array of properties
@@ -374,6 +450,16 @@ fn determine_failed_properties(properties: &[Property]) -> FailedProperties {
     }
 }
 
+fn determine_failed_covers(properties: &[Property]) -> CoversStatus {
+    let cover_properties: Vec<&Property> =
+        properties.iter().filter(|prop| prop.property_class() == "cover").collect();
+    if cover_properties.iter().all(|prop| prop.status == CheckStatus::Satisfied) {
+        CoversStatus::AllSatisfied
+    } else {
+        CoversStatus::Other
+    }
+}
+
 /// Solve Unwind Value from conflicting inputs of unwind values. (--default-unwind, annotation-unwind, --unwind)
 pub fn resolve_unwind_value(
     args: &VerificationArgs,
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index 8da67dae7ab1..d8ae10beefb3 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::args::OutputFormat;
-use crate::call_cbmc::{FailedProperties, VerificationStatus};
+use crate::call_cbmc::{GlobalCondition, VerificationStatus};
 use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem};
 use console::style;
 use once_cell::sync::Lazy;
@@ -245,8 +245,7 @@ fn format_item_terse(_item: &ParserItem) -> Option<String> {
 pub fn format_result(
     properties: &Vec<Property>,
     status: VerificationStatus,
-    should_panic: bool,
-    failed_properties: FailedProperties,
+    global_conditions: &Vec<GlobalCondition>,
     show_checks: bool,
 ) -> String {
     let mut result_str = String::new();
@@ -322,6 +321,27 @@ pub fn format_result(
         index += 1;
     }
 
+    let enabled_global_conditions = !global_conditions
+        .iter()
+        .filter(|cond| cond.enabled())
+        .collect::<Vec<&GlobalCondition>>()
+        .is_empty();
+
+    let mut global_condition_failures = false;
+    if enabled_global_conditions {
+        result_str.push_str("GLOBAL CONDITIONS:\n");
+        for cond in global_conditions {
+            if cond.enabled() {
+                let cond_status = if cond.passed() {
+                    CheckStatus::Success
+                } else {
+                    global_condition_failures = true;
+                    CheckStatus::Failure
+                };
+                result_str.push_str(&format!("- {}: {}\n", cond.name(), cond_status));
+            }
+        }
+    }
     if show_checks {
         result_str.push_str("\nSUMMARY:");
     } else {
@@ -388,19 +408,14 @@ pub fn format_result(
     } else {
         style("FAILED").red()
     };
-    let should_panic_info = if should_panic {
-        match failed_properties {
-            FailedProperties::None => " (encountered no panics, but at least one was expected)",
-            FailedProperties::PanicsOnly => " (encountered one or more panics as expected)",
-            FailedProperties::Other => {
-                " (encountered failures other than panics, which were unexpected)"
-            }
-        }
-    } else {
-        ""
-    };
-    let overall_result = format!("\nVERIFICATION:- {verification_result}{should_panic_info}\n");
+
+    let overall_result = format!("\nVERIFICATION:- {verification_result}");
+
     result_str.push_str(&overall_result);
+    if global_condition_failures {
+        result_str.push_str(" (one or more global conditions failed)");
+    }
+    result_str.push('\n');
 
     // Ideally, we should generate two `ParserItem::Message` and push them
     // into the parser iterator so they are the next messages to be processed.
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index f1f0befc4ddd..5b795e1045b9 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -94,10 +94,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, harness.attributes.should_panic)
-                );
+                println!("{}", result.render(&self.args.output_format));
             }
             self.gen_and_add_concrete_playback(harness, &mut result)?;
             Ok(result)

From 9a0b69fc118535ef11fc4baa70c9bf0ac7233a38 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 12 Jun 2023 15:30:26 +0000
Subject: [PATCH 02/14] Ammend `ui` test cases for `kani::should_panic`
 attribute

---
 tests/ui/should-panic-attribute/expected-panics/expected     | 4 +++-
 tests/ui/should-panic-attribute/no-panics/expected           | 5 +++--
 tests/ui/should-panic-attribute/unexpected-failures/expected | 5 ++++-
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/tests/ui/should-panic-attribute/expected-panics/expected b/tests/ui/should-panic-attribute/expected-panics/expected
index c6a6fa5c6c48..8d7e7f6f84d2 100644
--- a/tests/ui/should-panic-attribute/expected-panics/expected
+++ b/tests/ui/should-panic-attribute/expected-panics/expected
@@ -1,4 +1,6 @@
  ** 2 of 2 failed\
 Failed Checks: panicked on the `if` branch!
 Failed Checks: panicked on the `else` branch!
-VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+GLOBAL CONDITIONS:\
+- should_panic: SUCCESS
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/should-panic-attribute/no-panics/expected b/tests/ui/should-panic-attribute/no-panics/expected
index be42df7fb7f6..0ed53de132fe 100644
--- a/tests/ui/should-panic-attribute/no-panics/expected
+++ b/tests/ui/should-panic-attribute/no-panics/expected
@@ -1,5 +1,6 @@
 check.assertion\
 SUCCESS\
 assertion failed: 1 + 1 == 2
-
-VERIFICATION:- FAILED (encountered no panics, but at least one was expected)
+GLOBAL CONDITIONS:\
+- should_panic: FAILURE
+VERIFICATION:- FAILED
diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected
index 6cd10b4bafd5..fa82e0206dfe 100644
--- a/tests/ui/should-panic-attribute/unexpected-failures/expected
+++ b/tests/ui/should-panic-attribute/unexpected-failures/expected
@@ -2,8 +2,11 @@ undefined-shift\
 Status: FAILURE\
 Description: "shift distance too large"
 
+GLOBAL CONDITIONS:\
+- should_panic: FAILURE
+
 Failed Checks: panicked on the `1` arm!
 Failed Checks: panicked on the `0` arm!
 Failed Checks: shift distance too large
 
-VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
+VERIFICATION:- FAILED

From 654cf17667efb19e083ee6011e19e63ea495791e Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 12 Jun 2023 15:49:55 +0000
Subject: [PATCH 03/14] Add reasons to global condition status

---
 kani-driver/src/call_cbmc.rs              | 16 ++++++++++++++++
 kani-driver/src/cbmc_property_renderer.rs |  2 +-
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 7de2620be2cd..b6ab0591f71d 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -70,6 +70,22 @@ impl GlobalCondition {
             Self::FailUncoverable { status, .. } => *status == CoversStatus::AllSatisfied,
         }
     }
+
+    pub fn reason(&self) -> &str {
+        match &self {
+            Self::ShouldPanic { status, .. } =>
+                match *status {
+                    FailedProperties::None => "encountered no panics, but at least one was expected",
+                    FailedProperties::PanicsOnly => "encountered one or more panics as expected",
+                    FailedProperties::Other => "encountered failures other than panics, which were unexpected",
+                }
+            Self::FailUncoverable { status, .. } =>
+                match *status {
+                    CoversStatus::AllSatisfied => "all cover statements were satisfied as expected",
+                    CoversStatus::Other => "encountered one or more cover statements which were not satisfied",
+                }
+        }
+    }
 }
 
 /// Our (kani-driver) notions of CBMC results.
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index d8ae10beefb3..59840a86856e 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -338,7 +338,7 @@ pub fn format_result(
                     global_condition_failures = true;
                     CheckStatus::Failure
                 };
-                result_str.push_str(&format!("- {}: {}\n", cond.name(), cond_status));
+                result_str.push_str(&format!(" - {}: {} ({})\n", cond.name(), cond_status, cond.reason()));
             }
         }
     }

From 50ae10bfa296ee7422675de26a107ad4dc9695b0 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 12 Jun 2023 17:25:36 +0000
Subject: [PATCH 04/14] Format previous changes

---
 kani-driver/src/call_cbmc.rs              | 20 +++++++++++---------
 kani-driver/src/cbmc_property_renderer.rs |  7 ++++++-
 2 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index b6ab0591f71d..7c0e7b9be79b 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -73,17 +73,19 @@ impl GlobalCondition {
 
     pub fn reason(&self) -> &str {
         match &self {
-            Self::ShouldPanic { status, .. } =>
-                match *status {
-                    FailedProperties::None => "encountered no panics, but at least one was expected",
-                    FailedProperties::PanicsOnly => "encountered one or more panics as expected",
-                    FailedProperties::Other => "encountered failures other than panics, which were unexpected",
+            Self::ShouldPanic { status, .. } => match *status {
+                FailedProperties::None => "encountered no panics, but at least one was expected",
+                FailedProperties::PanicsOnly => "encountered one or more panics as expected",
+                FailedProperties::Other => {
+                    "encountered failures other than panics, which were unexpected"
                 }
-            Self::FailUncoverable { status, .. } =>
-                match *status {
-                    CoversStatus::AllSatisfied => "all cover statements were satisfied as expected",
-                    CoversStatus::Other => "encountered one or more cover statements which were not satisfied",
+            },
+            Self::FailUncoverable { status, .. } => match *status {
+                CoversStatus::AllSatisfied => "all cover statements were satisfied as expected",
+                CoversStatus::Other => {
+                    "encountered one or more cover statements which were not satisfied"
                 }
+            },
         }
     }
 }
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index 59840a86856e..fa3eb66b8bf6 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -338,7 +338,12 @@ pub fn format_result(
                     global_condition_failures = true;
                     CheckStatus::Failure
                 };
-                result_str.push_str(&format!(" - {}: {} ({})\n", cond.name(), cond_status, cond.reason()));
+                result_str.push_str(&format!(
+                    " - {}: {} ({})\n",
+                    cond.name(),
+                    cond_status,
+                    cond.reason()
+                ));
             }
         }
     }

From dcddff95e8b2856fb8c793ec70f3d8fff75ed3ad Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 12 Jun 2023 17:26:22 +0000
Subject: [PATCH 05/14] Add test cases for `--fail-uncoverable`

---
 tests/ui/fail-uncoverable/all-covered/expected | 10 ++++++++++
 tests/ui/fail-uncoverable/all-covered/test.rs  | 17 +++++++++++++++++
 tests/ui/fail-uncoverable/uncoverable/expected |  7 +++++++
 tests/ui/fail-uncoverable/uncoverable/test.rs  | 15 +++++++++++++++
 tests/ui/fail-uncoverable/unsatisfied/expected |  7 +++++++
 tests/ui/fail-uncoverable/unsatisfied/test.rs  | 13 +++++++++++++
 6 files changed, 69 insertions(+)
 create mode 100644 tests/ui/fail-uncoverable/all-covered/expected
 create mode 100644 tests/ui/fail-uncoverable/all-covered/test.rs
 create mode 100644 tests/ui/fail-uncoverable/uncoverable/expected
 create mode 100644 tests/ui/fail-uncoverable/uncoverable/test.rs
 create mode 100644 tests/ui/fail-uncoverable/unsatisfied/expected
 create mode 100644 tests/ui/fail-uncoverable/unsatisfied/test.rs

diff --git a/tests/ui/fail-uncoverable/all-covered/expected b/tests/ui/fail-uncoverable/all-covered/expected
new file mode 100644
index 000000000000..08619ce04aae
--- /dev/null
+++ b/tests/ui/fail-uncoverable/all-covered/expected
@@ -0,0 +1,10 @@
+
+harness1.cover.1\
+Status: SATISFIED\
+Description: "cover location"
+harness2.cover.1\
+Status: SATISFIED\
+Description: "cover condition: x == 1"
+GLOBAL CONDITIONS:\
+ - fail_uncoverable: SUCCESS (all cover statements were satisfied as expected)
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
\ No newline at end of file
diff --git a/tests/ui/fail-uncoverable/all-covered/test.rs b/tests/ui/fail-uncoverable/all-covered/test.rs
new file mode 100644
index 000000000000..37f7403bce65
--- /dev/null
+++ b/tests/ui/fail-uncoverable/all-covered/test.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --fail-uncoverable
+
+//! Checks that all cover statements are covered/satisfied and
+//! `--fail-uncoverable` doesn't cause failures.
+
+#[kani::proof]
+fn harness1() {
+    kani::cover!();
+}
+
+#[kani::proof]
+fn harness2() {
+    let x: u32 = kani::any();
+    kani::cover!(x == 1);
+}
diff --git a/tests/ui/fail-uncoverable/uncoverable/expected b/tests/ui/fail-uncoverable/uncoverable/expected
new file mode 100644
index 000000000000..3bbe34073732
--- /dev/null
+++ b/tests/ui/fail-uncoverable/uncoverable/expected
@@ -0,0 +1,7 @@
+
+harness_uncoverable.cover.1\
+Status: UNREACHABLE\
+Description: "cover location"
+GLOBAL CONDITIONS:\
+ - fail_uncoverable: FAILURE (encountered one or more cover statements which were not satisfied)
+VERIFICATION:- FAILED (one or more global conditions failed)
\ No newline at end of file
diff --git a/tests/ui/fail-uncoverable/uncoverable/test.rs b/tests/ui/fail-uncoverable/uncoverable/test.rs
new file mode 100644
index 000000000000..480f47cfb2a5
--- /dev/null
+++ b/tests/ui/fail-uncoverable/uncoverable/test.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --fail-uncoverable
+
+//! Checks that the `--fail-uncoverable` option cause a failure due to a cover
+//! statement not being covered.
+
+#[kani::proof]
+fn harness_uncoverable() {
+    let x: i32 = kani::any();
+    kani::assume(x >= 0);
+    if x < 0 {
+        kani::cover!();
+    }
+}
diff --git a/tests/ui/fail-uncoverable/unsatisfied/expected b/tests/ui/fail-uncoverable/unsatisfied/expected
new file mode 100644
index 000000000000..87de3ca9d023
--- /dev/null
+++ b/tests/ui/fail-uncoverable/unsatisfied/expected
@@ -0,0 +1,7 @@
+
+harness_unsatisfied.cover.1\
+Status: UNSATISFIABLE\
+Description: "cover condition: x == -1"
+GLOBAL CONDITIONS:\
+ - fail_uncoverable: FAILURE (encountered one or more cover statements which were not satisfied)
+VERIFICATION:- FAILED (one or more global conditions failed)
\ No newline at end of file
diff --git a/tests/ui/fail-uncoverable/unsatisfied/test.rs b/tests/ui/fail-uncoverable/unsatisfied/test.rs
new file mode 100644
index 000000000000..419dbcb16876
--- /dev/null
+++ b/tests/ui/fail-uncoverable/unsatisfied/test.rs
@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --fail-uncoverable
+
+//! Checks that the `--fail-uncoverable` option cause a failure due to a cover
+//! statement not being satisfied.
+
+#[kani::proof]
+fn harness_unsatisfied() {
+    let x: i32 = kani::any();
+    kani::assume(x >= 0);
+    kani::cover!(x == -1);
+}

From 91bd225b6cee47faa9c3d648ab6f9017f09bf53c Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 15 Jun 2023 18:33:48 +0000
Subject: [PATCH 06/14] Clean up some code, rename methods

---
 kani-driver/src/call_cbmc.rs | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 7c0e7b9be79b..1f0debfd0c9f 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -315,8 +315,7 @@ impl VerificationResult {
     ) -> VerificationResult {
         let runtime = start_time.elapsed();
         let (items, results) = extract_results(output.processed_items);
-        // let global_conditions: Vec<GlobalCondition> = vec![GlobalCondition::ShouldPanic { enabled: should_panic, status: None },
-        // FailUncoverable { enabled: fail_uncoverable, status: None }];
+
         if let Some(results) = results {
             let (status, global_conditions) =
                 verification_outcome_from_properties(&results, should_panic, fail_uncoverable);
@@ -402,25 +401,27 @@ fn verification_outcome_from_properties(
     should_panic: bool,
     fail_uncoverable: bool,
 ) -> (VerificationStatus, Vec<GlobalCondition>) {
-    let should_panic_cond = should_panic_cond(should_panic, properties);
-    let fail_uncoverable_cond = fail_uncoverable_cond(fail_uncoverable, properties);
-    // let failed_covers = determine_failed_covers(properties);
+    // Compute the results for all global conditions
+    let should_panic_cond = compute_should_panic_condition(should_panic, properties);
+    let fail_uncoverable_cond = compute_fail_uncoverable_condition(fail_uncoverable, properties);
+    // Create a vector with results for global conditions
     let global_conditions = vec![should_panic_cond, fail_uncoverable_cond];
-    // global_conditions.push();
+    // Determine the overall outcome taking into account all global conditions
     let status = outcome_from_global_conditions(properties, &global_conditions);
     (status, global_conditions)
 }
 
-fn should_panic_cond(enabled: bool, properties: &[Property]) -> GlobalCondition {
+fn compute_should_panic_condition(enabled: bool, properties: &[Property]) -> GlobalCondition {
     let failed_properties = determine_failed_properties(properties);
     GlobalCondition::ShouldPanic { enabled, status: failed_properties }
 }
 
-fn fail_uncoverable_cond(enabled: bool, properties: &[Property]) -> GlobalCondition {
-    let failed_covers = determine_failed_covers(properties);
+fn compute_fail_uncoverable_condition(enabled: bool, properties: &[Property]) -> GlobalCondition {
+    let failed_covers = determine_satisfiable_covers(properties);
     GlobalCondition::FailUncoverable { enabled, status: failed_covers }
 }
 
+// Determine the overall verification result considering the enabled global conditions
 fn outcome_from_global_conditions(
     properties: &[Property],
     global_conditions: &[GlobalCondition],
@@ -468,7 +469,8 @@ fn determine_failed_properties(properties: &[Property]) -> FailedProperties {
     }
 }
 
-fn determine_failed_covers(properties: &[Property]) -> CoversStatus {
+/// Determines the `CoverStatus` variant that corresponds to an array of properties
+fn determine_satisfiable_covers(properties: &[Property]) -> CoversStatus {
     let cover_properties: Vec<&Property> =
         properties.iter().filter(|prop| prop.property_class() == "cover").collect();
     if cover_properties.iter().all(|prop| prop.status == CheckStatus::Satisfied) {

From 4101f6dcccacab2088f6d1a377732c6b15ff99e7 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 15 Jun 2023 18:34:41 +0000
Subject: [PATCH 07/14] Add global conditions' failure message to one test

---
 tests/ui/should-panic-attribute/no-panics/expected | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/ui/should-panic-attribute/no-panics/expected b/tests/ui/should-panic-attribute/no-panics/expected
index 0ed53de132fe..5d26ae9315b2 100644
--- a/tests/ui/should-panic-attribute/no-panics/expected
+++ b/tests/ui/should-panic-attribute/no-panics/expected
@@ -3,4 +3,4 @@ SUCCESS\
 assertion failed: 1 + 1 == 2
 GLOBAL CONDITIONS:\
 - should_panic: FAILURE
-VERIFICATION:- FAILED
+VERIFICATION:- FAILED (one or more global conditions failed)

From ec604a73e493e48cae6039449bae4df5b94b7ecd Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 15 Jun 2023 18:39:12 +0000
Subject: [PATCH 08/14] Add it to another `expected` test

---
 tests/ui/should-panic-attribute/unexpected-failures/expected | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected
index fa82e0206dfe..ccf3decb543f 100644
--- a/tests/ui/should-panic-attribute/unexpected-failures/expected
+++ b/tests/ui/should-panic-attribute/unexpected-failures/expected
@@ -9,4 +9,4 @@ Failed Checks: panicked on the `1` arm!
 Failed Checks: panicked on the `0` arm!
 Failed Checks: shift distance too large
 
-VERIFICATION:- FAILED
+VERIFICATION:- FAILED (one or more global conditions failed)

From b77937e68c79f1bb19f6458f72febd5f1e9b8c72 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 19 Jun 2023 17:16:15 +0000
Subject: [PATCH 09/14] Print failed checks for global conditions

---
 kani-driver/src/call_cbmc.rs              | 12 ++++++++++++
 kani-driver/src/cbmc_property_renderer.rs | 12 +++++++++---
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 1f0debfd0c9f..3aa3ab0e8c3b 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/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.
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index fa3eb66b8bf6..486592ff9400 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -332,11 +332,11 @@ 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",
@@ -344,6 +344,12 @@ pub fn format_result(
                     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);
+                    }
+                }
             }
         }
     }

From ed5d4ef44f5dfefcf5805b55b1f244b7fdd2e8f8 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Tue, 20 Jun 2023 15:49:13 +0000
Subject: [PATCH 10/14] Format

---
 kani-driver/src/call_cbmc.rs              | 26 +++++++++++++++++------
 kani-driver/src/cbmc_property_renderer.rs |  3 ++-
 2 files changed, 22 insertions(+), 7 deletions(-)

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

From b5b8447e7f4be7eba69d9515cce7f2fa2b200b17 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Wed, 3 Jan 2024 16:45:00 +0000
Subject: [PATCH 11/14] Adapt to work with coverage

---
 kani-driver/src/call_cbmc.rs              | 2 +-
 kani-driver/src/cbmc_property_renderer.rs | 5 ++---
 kani-driver/src/harness_runner.rs         | 8 +-------
 3 files changed, 4 insertions(+), 11 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index fc444e845d4b..f11174c18b22 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/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)
                 };
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index ac071ce65590..71d1d50d44bb 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/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);
 
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index a7987c292e54..51202faa4250 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/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)

From 1dda0edfdc9cdbe9fa5a0293064ea6005fc180b6 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Wed, 3 Jan 2024 17:30:10 +0000
Subject: [PATCH 12/14] Minor improvements in documentation

---
 kani-driver/src/call_cbmc.rs                  | 2 ++
 tests/ui/fail-uncoverable/all-covered/test.rs | 4 ++--
 tests/ui/fail-uncoverable/uncoverable/test.rs | 2 +-
 tests/ui/fail-uncoverable/unsatisfied/test.rs | 2 +-
 4 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index f11174c18b22..ae9883516bc8 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -472,7 +472,9 @@ fn outcome_from_global_conditions(
         .filter(|cond| cond.enabled())
         .collect::<Vec<&GlobalCondition>>()
         .is_empty();
+
     if !enabled_global_conditions {
+        // If no global conditions are enabled, the outcome only depends on failed properties
         let failed_properties = determine_failed_properties(properties);
         if failed_properties == FailedProperties::None {
             VerificationStatus::Success
diff --git a/tests/ui/fail-uncoverable/all-covered/test.rs b/tests/ui/fail-uncoverable/all-covered/test.rs
index 37f7403bce65..a9f5be67aa66 100644
--- a/tests/ui/fail-uncoverable/all-covered/test.rs
+++ b/tests/ui/fail-uncoverable/all-covered/test.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that all cover statements are covered/satisfied and
-//! `--fail-uncoverable` doesn't cause failures.
+//! Checks that all cover statements are satisfied and `--fail-uncoverable`
+//! doesn't cause failures.
 
 #[kani::proof]
 fn harness1() {
diff --git a/tests/ui/fail-uncoverable/uncoverable/test.rs b/tests/ui/fail-uncoverable/uncoverable/test.rs
index 480f47cfb2a5..386f5bf45ad3 100644
--- a/tests/ui/fail-uncoverable/uncoverable/test.rs
+++ b/tests/ui/fail-uncoverable/uncoverable/test.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option cause a failure due to a cover
+//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
 //! statement not being covered.
 
 #[kani::proof]
diff --git a/tests/ui/fail-uncoverable/unsatisfied/test.rs b/tests/ui/fail-uncoverable/unsatisfied/test.rs
index 419dbcb16876..e79b426c9426 100644
--- a/tests/ui/fail-uncoverable/unsatisfied/test.rs
+++ b/tests/ui/fail-uncoverable/unsatisfied/test.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option cause a failure due to a cover
+//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
 //! statement not being satisfied.
 
 #[kani::proof]

From fc081663b0d05c725e9652ca0e859c4d0ecc23e8 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Wed, 3 Jan 2024 21:29:45 +0000
Subject: [PATCH 13/14] Use full output lines in `ui` tests

---
 tests/ui/should-panic-attribute/expected-panics/expected     | 2 +-
 tests/ui/should-panic-attribute/no-panics/expected           | 2 +-
 tests/ui/should-panic-attribute/unexpected-failures/expected | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/ui/should-panic-attribute/expected-panics/expected b/tests/ui/should-panic-attribute/expected-panics/expected
index 62f0c5735039..83c2c0f2f95c 100644
--- a/tests/ui/should-panic-attribute/expected-panics/expected
+++ b/tests/ui/should-panic-attribute/expected-panics/expected
@@ -2,5 +2,5 @@
 Failed Checks: panicked on the `if` branch!
 Failed Checks: panicked on the `else` branch!
 GLOBAL CONDITIONS:\
-- should_panic: SUCCESS
+ - should_panic: SUCCESS (encountered one or more panics as expected)
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/should-panic-attribute/no-panics/expected b/tests/ui/should-panic-attribute/no-panics/expected
index 5d26ae9315b2..8ce1a5a34b67 100644
--- a/tests/ui/should-panic-attribute/no-panics/expected
+++ b/tests/ui/should-panic-attribute/no-panics/expected
@@ -2,5 +2,5 @@ check.assertion\
 SUCCESS\
 assertion failed: 1 + 1 == 2
 GLOBAL CONDITIONS:\
-- should_panic: FAILURE
+ - should_panic: FAILURE (encountered no panics, but at least one was expected)
 VERIFICATION:- FAILED (one or more global conditions failed)
diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected
index 80d67d93980a..909b3dafd87a 100644
--- a/tests/ui/should-panic-attribute/unexpected-failures/expected
+++ b/tests/ui/should-panic-attribute/unexpected-failures/expected
@@ -3,7 +3,7 @@ Status: FAILURE\
 Description: "attempt to shift by excessive shift distance"
 
 GLOBAL CONDITIONS:\
-- should_panic: FAILURE
+ - should_panic: FAILURE (encountered failures other than panics, which were unexpected)
 
 Failed Checks: panicked on the `1` arm!
 Failed Checks: panicked on the `0` arm!

From 12ecc4b5d7b6f99790bb4460106b823d4b477e4c Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Wed, 10 Jan 2024 23:09:17 +0000
Subject: [PATCH 14/14] Minor improvements in test descriptions

---
 tests/ui/fail-uncoverable/all-covered/test.rs | 4 ++--
 tests/ui/fail-uncoverable/uncoverable/test.rs | 6 ++++--
 tests/ui/fail-uncoverable/unsatisfied/test.rs | 7 +++++--
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/tests/ui/fail-uncoverable/all-covered/test.rs b/tests/ui/fail-uncoverable/all-covered/test.rs
index a9f5be67aa66..2708c2870590 100644
--- a/tests/ui/fail-uncoverable/all-covered/test.rs
+++ b/tests/ui/fail-uncoverable/all-covered/test.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that all cover statements are satisfied and `--fail-uncoverable`
-//! doesn't cause failures.
+//! Checks that all cover statements are satisfied and enabling
+//! `--fail-uncoverable` doesn't cause unexpected failures.
 
 #[kani::proof]
 fn harness1() {
diff --git a/tests/ui/fail-uncoverable/uncoverable/test.rs b/tests/ui/fail-uncoverable/uncoverable/test.rs
index 386f5bf45ad3..dfde7f6eedb3 100644
--- a/tests/ui/fail-uncoverable/uncoverable/test.rs
+++ b/tests/ui/fail-uncoverable/uncoverable/test.rs
@@ -2,8 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
-//! statement not being covered.
+//! Checks that enabling the `--fail-uncoverable` option triggers a
+//! condition-based failure due to a `cover` statement not being satisfied.
+//!
+//! Note: The `cover` statement isn't satisfied because it's unreachable.
 
 #[kani::proof]
 fn harness_uncoverable() {
diff --git a/tests/ui/fail-uncoverable/unsatisfied/test.rs b/tests/ui/fail-uncoverable/unsatisfied/test.rs
index e79b426c9426..a8e2bb689510 100644
--- a/tests/ui/fail-uncoverable/unsatisfied/test.rs
+++ b/tests/ui/fail-uncoverable/unsatisfied/test.rs
@@ -2,8 +2,11 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
-//! statement not being satisfied.
+//! Checks that enabling the `--fail-uncoverable` option triggers a
+//! condition-based failure due to a `cover` statement not being satisfied.
+//!
+//! Note: The `cover` statement isn't satisfied because the condition `x == -1`
+//! cannot be satisfied.
 
 #[kani::proof]
 fn harness_unsatisfied() {