The integration with the Rust coverage instrumentation being introduced in #3119 seems to work well for all cases except for function calls causing panics or other control-flow divergences. Take the following example:

14 fn some_function(a: u64, b: u64) -> bool{
15     if a > b { panic!(); false } else { true}
16 }
17
18 #[kani::proof]
19 fn panics() {
20    let a: u64 = kani::any();
21    let b: u64 = kani::any();
22    panic!();
23    assert!(some_function(a, b));
24 }

The instrumentation introduced in #3119 reports a single region for the whole function, which is considered to be covered:

Failed Checks: explicit panic
 File: "src/main.rs", line 15, in some_function

VERIFICATION:- FAILED

Source-based code coverage results:

src/main.rs (panics)
 * 19:1 - 24:2 COVERED

src/main.rs (some_function)
 * 14:1 - 15:13 COVERED
 * 15:16 - 15:24 COVERED
 * 15:41 - 16:2 COVERED

This is very relevant when using certain Kani APIs like kani::assume(...) because the code following it will be reported as being within the same (covered) region when actually that part might not being covered. For example, let's take the program:

1 #[kani::proof]
2 fn dummy() {
3     let x: u32 = kani::any();
4     kani::assume(false);
5     assert!(x == 2);
6 }

The results we currently obtain are:

src/main.rs (main)
 * 2:1 - 6:2 COVERED

which are incorrect. Instead, there should be:

1. One region from the beginning of the function to the end of the kani::assume(..) statement.
2. Another region containing the assert!(x == 2) statement which is actually unreachable during verification.

Note that this is an issue with the Rust coverage instrumentation, which assumes that function calls never panic. This assumption does result in a much more efficient instrumentation. According to this Zulip thread, the Rust team will attempt to lift this assumption and potentially provide options to disable the optimization. The issue tracking this work is mainly rust-lang/rust#78544.