only fail for undetermined if there are unwinding failures; fix docs

kani-driver/src/cbmc_property_renderer.rs

@@ -513,7 +513,7 @@ pub fn postprocess_result(properties: Vec<Property>, extra_ptr_checks: bool) ->
     let updated_properties =
         update_properties_with_reach_status(properties_filtered, has_fundamental_failures);
     let results_after_code_coverage = update_results_of_code_coverage_checks(updated_properties);
-    update_results_of_cover_checks(results_after_code_coverage)
+    update_results_of_cover_checks(results_after_code_coverage, has_failed_unwinding_asserts)
 }
 
 /// Determines if there is property with status `FAILURE` and the given description
@@ -649,8 +649,15 @@ fn update_results_of_code_coverage_checks(mut properties: Vec<Property>) -> Vec<
 /// `update_properties_with_reach_status` is called beforehand
 ///
 /// Although regular cover properties do not fail verification, contract cover properties do.
-/// If the assert(!cond) fails as expected, succeed; otherwise, fail.
-fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property> {
+/// If the assert(!cond) is unreachable or successful, then fail.
+/// Also fail if the status is undetermined and there are failed unwinding asserts; if we didn't unwind enough,
+/// we know that the postcondition is unreachable.
+/// If the status is undetermined for another reason (e.g., unsupported constructs), leave the result as undetermined.
+/// If the status is failure (as expected), succeed.
+fn update_results_of_cover_checks(
+    mut properties: Vec<Property>,
+    has_failed_unwinding_asserts: bool,
+) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_cover_property() {
             if prop.status == CheckStatus::Success {
@@ -661,7 +668,7 @@ fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property
         } else if prop.is_contract_cover_property() {
             if prop.status == CheckStatus::Unreachable
                 || prop.status == CheckStatus::Success
-                || prop.status == CheckStatus::Undetermined
+                || (prop.status == CheckStatus::Undetermined && has_failed_unwinding_asserts)
             {
                 prop.status = CheckStatus::Failure;
             } else if prop.status == CheckStatus::Failure {

library/kani_macros/src/sysroot/contracts/mod.rs

@@ -326,7 +326,7 @@
 //!                                let mut __kani_check_modify =
 //!                                    ||
 //!                                        {
-//!                                            kani::assume(divisor != 0);
+//!                                            kani::assume(*ptr < 100);
 //!                                            kani::internal::contract_cover(*ptr < 100, "The contract's precondition is satisfiable.");
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
@@ -395,6 +395,8 @@
 //!             let mut __kani_check_modify =
 //!                 ||
 //!                     {
+//!                         kani::assume(*ptr < 100);
+//!                         kani::internal::contract_cover(*ptr < 100, "The contract's precondition is satisfiable.");
 //!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                         let _wrapper_arg = (ptr as *const _,);

tests/expected/function-contract/cover_contract/undetermined_postcondition.expected

@@ -0,0 +1,9 @@
+
+contract_cover.2\
+	 - Status: UNDETERMINED\
+	 - Description: "The contract's postcondition is reachable."
+
+unsupported_construct.1\
+	 - Status: FAILURE
+
+VERIFICATION:- FAILED

tests/expected/function-contract/cover_contract/undetermined_postcondition.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test `cover_contract` functionality, which fails verification for a unsatisfiable precondition
+// or unreachable postcondition.
+// See https://github.com/model-checking/kani/issues/2793
+
+// Undetermined whether we can reach the postcondition because we encounter an unsupported construct.
+
+#[kani::proof_for_contract(unsupp)]
+fn undetermined_example() {
+    let mut x = 0;
+    unsupp(&mut x);
+    assert!(x == 0);
+}
+
+#[kani::requires(true)]
+#[kani::ensures(|res| *res == *x)]
+fn unsupp(x: &mut u8) -> u8 {
+    unsafe {
+        std::arch::asm!("nop");
+    }
+    *x
+}

tests/expected/function-contract/cover_contract/unreachable_postcondition.rs

@@ -2,12 +2,15 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-// Test `conver_contract` functionality, which fails verification for a vacuous precondition
+// Test `cover_contract` functionality, which fails verification for a unsatisfiable precondition
 // or unreachable postcondition.
 // See https://github.com/model-checking/kani/issues/2793
 
-// Unreachable postcondition.
+// Test that verification fails for an unreachable postcondition.
+
 // The precondition is satisfiable, but the postcondition is unreachable because the code panics.
+// Test that in the case where the postcondition check's property status is unreachable (because the function panics)
+// we change the status to failure.
 #[kani::requires(a > 5)]
 #[kani::ensures(|result: &u32| *result == a)]
 fn unreachable_postcondition(a: u32) -> u32 {
@@ -20,13 +23,15 @@ fn prove_unreachable_postcondition() {
     unreachable_postcondition(x);
 }
 
+// Unreachable postcondition because the function never returns.
+// Test that in the case where the postcondition check's property status is undetermined because of unwinding failures,
+// we change the status to failure.
 #[kani::ensures(|result: &u32| *result == 7)]
 fn never_return() -> u32 {
     loop {}
     7
 }
 
-// Unreachable postcondition because the function never returns
 #[kani::proof_for_contract(never_return)]
 #[kani::unwind(5)]
 fn prove_never_return() {

tests/expected/function-contract/cover_contract/vacuous_precondition.rs → tests/expected/function-contract/cover_contract/unsatisfiable_precondition.rs

@@ -2,11 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-// Test `conver_contract` functionality, which fails verification for a vacuous precondition
+// Test `cover_contract` functionality, which fails verification for an unsatisfiable precondition
 // or unreachable postcondition.
 // See https://github.com/model-checking/kani/issues/2793
 
-// Vacuous precondition; separate requires clauses
+// Test that verification fails for unsatisfiable preconditions.
+
+// Unsatisfiable precondition; separate requires clauses.
+// The postcondition is unreachable because of the unsatisfiable precondition.
 #[kani::requires(a > 5)]
 #[kani::requires(a < 4)]
 #[kani::ensures(|result: &u32| *result == a)]
@@ -20,7 +23,8 @@ fn prove_separate_requires() {
     separate_requires(x);
 }
 
-// Vacuous precondition; single requires clause
+// Unsatisfiable precondition; single requires clause
+// The postcondition is unreachable because of the unsatisfiable precondition.
 #[kani::requires(a > 5 && a < 4)]
 #[kani::ensures(|result: &u32| *result == a)]
 fn conjoined_requires(a: u32) -> u32 {