Address test related comments

tests/coverage/reachable/assert-false/expected

@@ -1,10 +1,8 @@
-coverage/reachable/assert-false/main.rs, 5, FULL
 coverage/reachable/assert-false/main.rs, 6, FULL
-coverage/reachable/assert-false/main.rs, 10, FULL
+coverage/reachable/assert-false/main.rs, 7, FULL
 coverage/reachable/assert-false/main.rs, 11, FULL
-coverage/reachable/assert-false/main.rs, 14, FULL
+coverage/reachable/assert-false/main.rs, 12, FULL
 coverage/reachable/assert-false/main.rs, 15, FULL
-coverage/reachable/assert-false/main.rs, 16, PARTIAL
+coverage/reachable/assert-false/main.rs, 16, FULL
+coverage/reachable/assert-false/main.rs, 17, PARTIAL
 coverage/reachable/assert-false/main.rs, 19, FULL
-coverage/reachable/assert-false/main.rs, 20, PARTIAL
-coverage/reachable/assert-false/main.rs, 22, FULL

tests/coverage/reachable/assert-false/main.rs

@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// Check that the assert is reported as PARTIAL for having both REACHABLE and UNREACHABLE checks
 fn any_bool() -> bool {
  kani::any()
 }
@@ -15,14 +16,4 @@ fn main() {
  let s = "Fail with custom runtime message";
  assert!(false, "{}", s);
  }
-
- if any_bool() {
- assert!(false, "Fail with custom static message");
- }
-}
-
-#[inline(always)]
-#[track_caller]
-fn check_caller(b: bool) {
- assert!(b);
 }

tests/coverage/unreachable/compare/expected

@@ -1,7 +1,7 @@
-coverage/unreachable/compare/main.rs, 5, PARTIAL
-coverage/unreachable/compare/main.rs, 6, FULL
-coverage/unreachable/compare/main.rs, 10, FULL
+coverage/unreachable/compare/main.rs, 6, PARTIAL
+coverage/unreachable/compare/main.rs, 7, FULL
 coverage/unreachable/compare/main.rs, 11, FULL
 coverage/unreachable/compare/main.rs, 12, FULL
 coverage/unreachable/compare/main.rs, 13, FULL
-coverage/unreachable/compare/main.rs, 15, FULL
+coverage/unreachable/compare/main.rs, 14, FULL
+coverage/unreachable/compare/main.rs, 16, FULL

tests/coverage/unreachable/compare/main.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 fn compare(x: u16, y: u16) -> u16 {
+ // The line below should be reported as PARTIAL for having both REACHABLE and UNREACHABLE checks
  if x >= y { 1 } else { 0 }
 }
 

tests/coverage/unreachable/divide/expected

@@ -1,5 +1,5 @@
-coverage/unreachable/divide/main.rs, 5, FULL
 coverage/unreachable/divide/main.rs, 6, FULL
+coverage/unreachable/divide/main.rs, 7, FULL
 coverage/unreachable/divide/main.rs, 9, NONE
 coverage/unreachable/divide/main.rs, 11, FULL
 coverage/unreachable/divide/main.rs, 15, FULL

tests/coverage/unreachable/divide/main.rs

@@ -1,17 +1,19 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// Test that checks for UNREACHABLE panics. The panic is reported as NONE for the assumption that the divisor is not zero.
 fn divide(a: i32, b: i32) -> i32 {
  if b != 0 {
  return a / b;
  } else {
- // This part is unreachable since b != 0 was already checked.
  panic!("Division by zero");
  }
 }
 
 #[kani::proof]
 fn main() {
- let result = divide(10, 2);
+ let y: i32 = kani::any();
+ kani::assume(y != 0);
+ let result = divide(10, y);
  assert_eq!(result, 5);
 }

tests/coverage/unreachable/if-statement/expected

@@ -1,10 +1,10 @@
 coverage/unreachable/if-statement/main.rs, 5, FULL
-coverage/unreachable/if-statement/main.rs, 6, PARTIAL
-coverage/unreachable/if-statement/main.rs, 7, NONE
+coverage/unreachable/if-statement/main.rs, 7, PARTIAL
 coverage/unreachable/if-statement/main.rs, 8, NONE
-coverage/unreachable/if-statement/main.rs, 10, NONE
-coverage/unreachable/if-statement/main.rs, 12, FULL
-coverage/unreachable/if-statement/main.rs, 16, FULL
+coverage/unreachable/if-statement/main.rs, 9, NONE
+coverage/unreachable/if-statement/main.rs, 11, NONE
+coverage/unreachable/if-statement/main.rs, 13, FULL
 coverage/unreachable/if-statement/main.rs, 17, FULL
 coverage/unreachable/if-statement/main.rs, 18, FULL
 coverage/unreachable/if-statement/main.rs, 19, FULL
+coverage/unreachable/if-statement/main.rs, 20, FULL

tests/coverage/unreachable/if-statement/main.rs

@@ -3,6 +3,7 @@
 
 fn check_number(num: i32) -> &'static str {
  if num > 0 {
+ // The line is partially covered because the if statement is UNREACHABLE while the else statement is reachable
  if num % 2 == 0 { "Positive and Even" } else { "Positive and Odd" }
  } else if num < 0 {
  "Negative"

tests/coverage/unreachable/variant/expected

@@ -1,9 +1,10 @@
-coverage/unreachable/variant/main.rs, 12, PARTIAL
+coverage/unreachable/variant/main.rs, 12, FULL
 coverage/unreachable/variant/main.rs, 13, NONE
 coverage/unreachable/variant/main.rs, 14, NONE
 coverage/unreachable/variant/main.rs, 15, FULL
 coverage/unreachable/variant/main.rs, 16, NONE
-coverage/unreachable/variant/main.rs, 19, FULL
-coverage/unreachable/variant/main.rs, 23, FULL
+coverage/unreachable/variant/main.rs, 18, NONE
+coverage/unreachable/variant/main.rs, 20, FULL
 coverage/unreachable/variant/main.rs, 24, FULL
 coverage/unreachable/variant/main.rs, 25, FULL
+coverage/unreachable/variant/main.rs, 26, FULL

tests/coverage/unreachable/variant/main.rs

@@ -15,6 +15,7 @@ fn print_direction(dir: Direction) {
  Direction::Left => println!("Going left!"),
  Direction::Right => println!("Going right!"),
  // This part is unreachable since we cover all variants in the match.
+ _ => {}
  }
 }