From 8c1784946f3adf4b820d238f95e8865a5af229ab Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Tue, 27 Aug 2024 14:35:00 -0400
Subject: [PATCH] Adopt Rust's source-based code coverage instrumentation
 (#3119)

This PR replaces the line-based coverage instrumentation we introduced
in #2609 with the standard source-based code coverage instrumentation
performed by the Rust compiler.

As a result, we now insert code coverage checks in the
`StatementKind::Coverage(..)` statements produced by the Rust compiler
during compilation. These checks include coverage-relevant
information[^note-internal] such as the coverage counter/expression they
represent [^note-instrument]. Both the coverage metadata (`kanimap`) and
coverage results (`kaniraw`) are saved into files after the verification
stage.

Unfortunately, we currently have a chicken-egg problem with this PR and
#3121, where we introduce a tool named `kani-cov` to postprocess
coverage results. As explained in #3143, `kani-cov` is expected to be an
alias for the `cov` subcommand and provide most of the postprocessing
features for coverage-related purposes. But, the tool will likely be
introduced after this change. Therefore, we propose to temporarily print
a list of the regions in each function with their associated coverage
status (i.e., `COVERED` or `UNCOVERED`).

### Source-based code coverage: An example

The main advantage of source-based coverage results is their precision
with respect to the source code. The [Source-based Code
Coverage](https://clang.llvm.org/docs/SourceBasedCodeCoverage.html)
documentation explains more details about the LLVM coverage workflow and
its different options.

For example, let's take this Rust code:
```rust
1 fn _other_function() {
2    println!("Hello, world!");
3 }
4
5 fn test_cov(val: u32) -> bool {
6     if val < 3 || val == 42 {
7         true
8     } else {
9         false
10    }
11 }
12
13 #[cfg_attr(kani, kani::proof)]
14 fn main() {
15    let test1 = test_cov(1);
16    let test2 = test_cov(2);
17    assert!(test1);
18    assert!(test2);
19 }
```

Compiling and running the program with `rustc` and the `-C
instrument-coverage` flag, and using the LLVM tools can get us the
following coverage result:


![Image](https://github.com/model-checking/kani/assets/73246657/9070e390-6e0b-4add-828d-d9f9caacad07)


In contrast, the `cargo kani --coverage -Zsource-coverage` command
currently generates:

```
src/main.rs (main)
 * 14:1 - 19:2 COVERED

src/main.rs (test_cov)
 * 5:1 - 6:15 COVERED
 * 6:19 - 6:28 UNCOVERED
 * 7:9 - 7:13 COVERED
 * 9:9 - 9:14 UNCOVERED
 * 11:1 - 11:2 COVERED
```

which is a verification-based coverage result almost equivalent to the
runtime coverage results.

### Benchmarking

We have evaluated the performance impact of the instrumentation using
the `kani-perf.sh` suite (14 benchmarks). For each test, we compare the
average time to run standard verification against the average time to
run verification with the source-based code coverage feature
enabled[^note-line-evaluation].

The evaluation has been performed on an EC2 `m5a.4xlarge` instance
running Ubuntu 22.04. The experimental data has been obtained by running
the `kani-perf.sh` script 10 times for each version (`only verification`
and `verification + coverage`), computing the average and standard
deviation. We've split this data into `small` (tests taking 60s or less)
and `large` (tests taking more than 60s) and drawn the two graphs below.

#### Performance comparison - `small` benchmarks


![performance_comparison_small](https://github.com/user-attachments/assets/679cf412-0193-4b0c-a78c-2d0fb702706f)

#### Performance comparison - `large` benchmarks


![performance_comparison_large](https://github.com/user-attachments/assets/4bb5a895-7f57-49e0-86b5-5fea67fad939)

#### Comments on performance

Looking at the small tests, the performance impact seems negligible in
such cases. The difference is more noticeable in the large tests, where
the time to run verification and coverage can take 2x or even more. It
wouldn't be surprising that, as programs become larger, the complexity
of the coverage checking grows exponentially as well. However, since
most verification jobs don't take longer than 30min (1800s), it's OK to
say that coverage checking represents a 100-200% slowdown in the worst
case w.r.t. standard verification.

It's also worth noting a few other things:
* The standard deviation remains similar in most cases, meaning that the
coverage feature doesn't have an impact on their stability.
* We haven't tried any SAT solvers other than the ones used by default
for each benchmark. It's possible that other solvers perform
better/worse with the coverage feature enabled.

### Call-outs
 * The soundness issue documented in #3441.
* The issue with saving coverage mappings for non-reachable functions
documented in #3445.
* I've modified the test cases in `tests/coverage/` to test this
feature. Since this technique is simpler, we don't need that many test
cases. However, it's possible I've left some test cases which don't
contribute much. Please let me know if you want to add/remove a test
case.

[^note-internal]: The coverage mappings can't be accessed through the
StableMIR interface so we retrieve them through the internal API.

[^note-instrument]: The instrumentation replaces certain counters with
expressions based on other counters when possible to avoid a part of the
runtime overhead. More details can be found
[here](https://github.com/rust-lang/rustc-dev-guide/blob/master/src/llvm-coverage-instrumentation.md#mir-pass-instrumentcoverage).
Unfortunately, we can't avoid instrumenting expressions at the moment.

[^note-line-evaluation]: We have not compared performance against the
line-based code coverage feature because it doesn't seem worth it. The
line-based coverage feature is guaranteed to include more coverage
checks than the source-based one for any function. In addition,
source-based results are more precise than line-based ones. So this
change represents both a quantitative and qualitative improvement.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 Cargo.lock                                    |  53 ++++++
 .../codegen_cprover_gotoc/codegen/assert.rs   |  16 +-
 .../codegen_cprover_gotoc/codegen/block.rs    |  33 +---
 .../codegen_cprover_gotoc/codegen/function.rs |  71 +++++++
 .../codegen/statement.rs                      |  19 +-
 kani-driver/Cargo.toml                        |   1 +
 kani-driver/src/args/mod.rs                   |   4 +-
 kani-driver/src/call_cargo.rs                 |   2 +-
 kani-driver/src/call_cbmc.rs                  | 100 +++++++++-
 kani-driver/src/call_single_file.rs           |   5 +
 kani-driver/src/cbmc_output_parser.rs         |   4 +-
 kani-driver/src/cbmc_property_renderer.rs     |  74 ++------
 kani-driver/src/coverage/cov_results.rs       |  96 ++++++++++
 kani-driver/src/coverage/cov_session.rs       | 176 ++++++++++++++++++
 kani-driver/src/coverage/mod.rs               |   5 +
 kani-driver/src/harness_runner.rs             |  17 +-
 kani-driver/src/main.rs                       |  19 ++
 kani-driver/src/project.rs                    |  18 +-
 kani_metadata/src/unstable.rs                 |   5 +-
 tests/coverage/abort/expected                 |  13 ++
 .../coverage/{unreachable => }/abort/main.rs  |   0
 tests/coverage/assert/expected                |   9 +
 .../coverage/{unreachable => }/assert/test.rs |   0
 tests/coverage/assert_eq/expected             |   8 +
 .../{unreachable => }/assert_eq/test.rs       |   0
 tests/coverage/assert_ne/expected             |   9 +
 .../{unreachable => }/assert_ne/test.rs       |   0
 tests/coverage/break/expected                 |  13 ++
 .../coverage/{unreachable => }/break/main.rs  |   2 +-
 tests/coverage/compare/expected               |  11 ++
 .../{unreachable => }/compare/main.rs         |   2 +-
 tests/coverage/contradiction/expected         |   9 +
 .../{unreachable => }/contradiction/main.rs   |   0
 tests/coverage/debug-assert/expected          |  10 +
 tests/coverage/debug-assert/main.rs           |  15 ++
 tests/coverage/div-zero/expected              |   9 +
 .../reachable_pass => div-zero}/test.rs       |   2 +-
 tests/coverage/early-return/expected          |  12 ++
 .../{unreachable => }/early-return/main.rs    |   0
 tests/coverage/if-statement-multi/expected    |  11 ++
 tests/coverage/if-statement-multi/test.rs     |  26 +++
 tests/coverage/if-statement/expected          |  14 ++
 .../{unreachable => }/if-statement/main.rs    |   2 +-
 .../assert_uncovered_end/expected             |   9 +
 .../known_issues/assert_uncovered_end/test.rs |  14 ++
 .../known_issues/assume_assert/expected       |   4 +
 .../known_issues/assume_assert/main.rs        |  15 ++
 .../known_issues/out-of-bounds/expected       |   7 +
 .../known_issues/out-of-bounds/test.rs        |  15 ++
 tests/coverage/known_issues/variant/expected  |  14 ++
 .../variant/main.rs                           |   5 +-
 tests/coverage/multiple-harnesses/expected    |  37 ++++
 .../multiple-harnesses/main.rs                |   0
 tests/coverage/overflow-failure/expected      |   9 +
 .../test.rs                                   |   4 +-
 .../coverage/overflow-full-coverage/expected  |   9 +
 .../test.rs                                   |   4 +-
 .../coverage/reachable/assert-false/expected  |   8 -
 tests/coverage/reachable/assert-false/main.rs |  19 --
 .../reachable/assert/reachable_pass/expected  |   4 -
 .../reachable/assert/reachable_pass/test.rs   |  10 -
 .../reachable/bounds/reachable_fail/expected  |   4 -
 .../reachable/bounds/reachable_fail/test.rs   |  11 --
 .../div-zero/reachable_fail/expected          |   4 -
 .../reachable/div-zero/reachable_fail/test.rs |  11 --
 .../div-zero/reachable_pass/expected          |   4 -
 .../overflow/reachable_fail/expected          |   5 -
 .../overflow/reachable_pass/expected          |   7 -
 .../rem-zero/reachable_fail/expected          |   4 -
 .../reachable/rem-zero/reachable_fail/test.rs |  11 --
 .../rem-zero/reachable_pass/expected          |   4 -
 .../reachable/rem-zero/reachable_pass/test.rs |  11 --
 tests/coverage/unreachable/abort/expected     |   7 -
 tests/coverage/unreachable/assert/expected    |   7 -
 tests/coverage/unreachable/assert_eq/expected |   5 -
 tests/coverage/unreachable/assert_ne/expected |   6 -
 .../unreachable/assume_assert/expected        |   4 -
 .../unreachable/assume_assert/main.rs         |   8 -
 tests/coverage/unreachable/bounds/expected    |   4 -
 tests/coverage/unreachable/bounds/test.rs     |  12 --
 tests/coverage/unreachable/break/expected     |   9 -
 tests/coverage/unreachable/check_id/expected  |  16 --
 tests/coverage/unreachable/check_id/main.rs   |  25 ---
 tests/coverage/unreachable/compare/expected   |   7 -
 .../unreachable/contradiction/expected        |   7 -
 .../unreachable/debug-assert/expected         |   4 -
 .../coverage/unreachable/debug-assert/main.rs |  10 -
 tests/coverage/unreachable/divide/expected    |   7 -
 tests/coverage/unreachable/divide/main.rs     |  19 --
 .../unreachable/early-return/expected         |  10 -
 .../unreachable/if-statement/expected         |  10 -
 .../unreachable/multiple-harnesses/expected   |  39 ----
 tests/coverage/unreachable/return/expected    |   8 -
 tests/coverage/unreachable/return/main.rs     |  17 --
 .../unreachable/tutorial_unreachable/expected |   5 -
 .../unreachable/tutorial_unreachable/main.rs  |  11 --
 tests/coverage/unreachable/variant/expected   |  10 -
 tests/coverage/unreachable/vectors/expected   |   6 -
 tests/coverage/unreachable/vectors/main.rs    |  19 --
 .../unreachable/while-loop-break/expected     |  11 --
 tests/coverage/while-loop-break/expected      |  13 ++
 .../while-loop-break/main.rs                  |   0
 tests/ui/save-coverage-results/expected       |   3 +
 tests/ui/save-coverage-results/test.rs        |  25 +++
 tools/compiletest/src/runtest.rs              |   2 +-
 105 files changed, 950 insertions(+), 554 deletions(-)
 create mode 100644 kani-driver/src/coverage/cov_results.rs
 create mode 100644 kani-driver/src/coverage/cov_session.rs
 create mode 100644 kani-driver/src/coverage/mod.rs
 create mode 100644 tests/coverage/abort/expected
 rename tests/coverage/{unreachable => }/abort/main.rs (100%)
 create mode 100644 tests/coverage/assert/expected
 rename tests/coverage/{unreachable => }/assert/test.rs (100%)
 create mode 100644 tests/coverage/assert_eq/expected
 rename tests/coverage/{unreachable => }/assert_eq/test.rs (100%)
 create mode 100644 tests/coverage/assert_ne/expected
 rename tests/coverage/{unreachable => }/assert_ne/test.rs (100%)
 create mode 100644 tests/coverage/break/expected
 rename tests/coverage/{unreachable => }/break/main.rs (82%)
 create mode 100644 tests/coverage/compare/expected
 rename tests/coverage/{unreachable => }/compare/main.rs (73%)
 create mode 100644 tests/coverage/contradiction/expected
 rename tests/coverage/{unreachable => }/contradiction/main.rs (100%)
 create mode 100644 tests/coverage/debug-assert/expected
 create mode 100644 tests/coverage/debug-assert/main.rs
 create mode 100644 tests/coverage/div-zero/expected
 rename tests/coverage/{reachable/div-zero/reachable_pass => div-zero}/test.rs (64%)
 create mode 100644 tests/coverage/early-return/expected
 rename tests/coverage/{unreachable => }/early-return/main.rs (100%)
 create mode 100644 tests/coverage/if-statement-multi/expected
 create mode 100644 tests/coverage/if-statement-multi/test.rs
 create mode 100644 tests/coverage/if-statement/expected
 rename tests/coverage/{unreachable => }/if-statement/main.rs (78%)
 create mode 100644 tests/coverage/known_issues/assert_uncovered_end/expected
 create mode 100644 tests/coverage/known_issues/assert_uncovered_end/test.rs
 create mode 100644 tests/coverage/known_issues/assume_assert/expected
 create mode 100644 tests/coverage/known_issues/assume_assert/main.rs
 create mode 100644 tests/coverage/known_issues/out-of-bounds/expected
 create mode 100644 tests/coverage/known_issues/out-of-bounds/test.rs
 create mode 100644 tests/coverage/known_issues/variant/expected
 rename tests/coverage/{unreachable => known_issues}/variant/main.rs (72%)
 create mode 100644 tests/coverage/multiple-harnesses/expected
 rename tests/coverage/{unreachable => }/multiple-harnesses/main.rs (100%)
 create mode 100644 tests/coverage/overflow-failure/expected
 rename tests/coverage/{reachable/overflow/reachable_fail => overflow-failure}/test.rs (66%)
 create mode 100644 tests/coverage/overflow-full-coverage/expected
 rename tests/coverage/{reachable/overflow/reachable_pass => overflow-full-coverage}/test.rs (62%)
 delete mode 100644 tests/coverage/reachable/assert-false/expected
 delete mode 100644 tests/coverage/reachable/assert-false/main.rs
 delete mode 100644 tests/coverage/reachable/assert/reachable_pass/expected
 delete mode 100644 tests/coverage/reachable/assert/reachable_pass/test.rs
 delete mode 100644 tests/coverage/reachable/bounds/reachable_fail/expected
 delete mode 100644 tests/coverage/reachable/bounds/reachable_fail/test.rs
 delete mode 100644 tests/coverage/reachable/div-zero/reachable_fail/expected
 delete mode 100644 tests/coverage/reachable/div-zero/reachable_fail/test.rs
 delete mode 100644 tests/coverage/reachable/div-zero/reachable_pass/expected
 delete mode 100644 tests/coverage/reachable/overflow/reachable_fail/expected
 delete mode 100644 tests/coverage/reachable/overflow/reachable_pass/expected
 delete mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/expected
 delete mode 100644 tests/coverage/reachable/rem-zero/reachable_fail/test.rs
 delete mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/expected
 delete mode 100644 tests/coverage/reachable/rem-zero/reachable_pass/test.rs
 delete mode 100644 tests/coverage/unreachable/abort/expected
 delete mode 100644 tests/coverage/unreachable/assert/expected
 delete mode 100644 tests/coverage/unreachable/assert_eq/expected
 delete mode 100644 tests/coverage/unreachable/assert_ne/expected
 delete mode 100644 tests/coverage/unreachable/assume_assert/expected
 delete mode 100644 tests/coverage/unreachable/assume_assert/main.rs
 delete mode 100644 tests/coverage/unreachable/bounds/expected
 delete mode 100644 tests/coverage/unreachable/bounds/test.rs
 delete mode 100644 tests/coverage/unreachable/break/expected
 delete mode 100644 tests/coverage/unreachable/check_id/expected
 delete mode 100644 tests/coverage/unreachable/check_id/main.rs
 delete mode 100644 tests/coverage/unreachable/compare/expected
 delete mode 100644 tests/coverage/unreachable/contradiction/expected
 delete mode 100644 tests/coverage/unreachable/debug-assert/expected
 delete mode 100644 tests/coverage/unreachable/debug-assert/main.rs
 delete mode 100644 tests/coverage/unreachable/divide/expected
 delete mode 100644 tests/coverage/unreachable/divide/main.rs
 delete mode 100644 tests/coverage/unreachable/early-return/expected
 delete mode 100644 tests/coverage/unreachable/if-statement/expected
 delete mode 100644 tests/coverage/unreachable/multiple-harnesses/expected
 delete mode 100644 tests/coverage/unreachable/return/expected
 delete mode 100644 tests/coverage/unreachable/return/main.rs
 delete mode 100644 tests/coverage/unreachable/tutorial_unreachable/expected
 delete mode 100644 tests/coverage/unreachable/tutorial_unreachable/main.rs
 delete mode 100644 tests/coverage/unreachable/variant/expected
 delete mode 100644 tests/coverage/unreachable/vectors/expected
 delete mode 100644 tests/coverage/unreachable/vectors/main.rs
 delete mode 100644 tests/coverage/unreachable/while-loop-break/expected
 create mode 100644 tests/coverage/while-loop-break/expected
 rename tests/coverage/{unreachable => }/while-loop-break/main.rs (100%)
 create mode 100644 tests/ui/save-coverage-results/expected
 create mode 100644 tests/ui/save-coverage-results/test.rs

diff --git a/Cargo.lock b/Cargo.lock
index d13ff68b32ff..0b8f681ae6c1 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -316,6 +316,15 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "deranged"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4"
+dependencies = [
+ "powerfmt",
+]
+
 [[package]]
 name = "either"
 version = "1.13.0"
@@ -500,6 +509,7 @@ dependencies = [
  "strum",
  "strum_macros",
  "tempfile",
+ "time",
  "toml",
  "tracing",
  "tracing-subscriber",
@@ -660,6 +670,12 @@ dependencies = [
  "num-traits",
 ]
 
+[[package]]
+name = "num-conv"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9"
+
 [[package]]
 name = "num-integer"
 version = "0.1.46"
@@ -767,6 +783,12 @@ version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02"
 
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
 [[package]]
 name = "ppv-lite86"
 version = "0.2.20"
@@ -1179,6 +1201,37 @@ dependencies = [
  "once_cell",
 ]
 
+[[package]]
+name = "time"
+version = "0.3.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
+dependencies = [
+ "deranged",
+ "itoa",
+ "num-conv",
+ "powerfmt",
+ "serde",
+ "time-core",
+ "time-macros",
+]
+
+[[package]]
+name = "time-core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
+
+[[package]]
+name = "time-macros"
+version = "0.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf"
+dependencies = [
+ "num-conv",
+ "time-core",
+]
+
 [[package]]
 name = "toml"
 version = "0.8.19"
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index f78cf3eba707..4ee81d0c7d3e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -21,6 +21,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
+use rustc_middle::mir::coverage::CodeRegion;
 use stable_mir::mir::{Place, ProjectionElem};
 use stable_mir::ty::{Span as SpanStable, TypeAndMut};
 use strum_macros::{AsRefStr, EnumString};
@@ -148,18 +149,19 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Generate a cover statement for code coverage reports.
-    pub fn codegen_coverage(&self, span: SpanStable) -> Stmt {
+    pub fn codegen_coverage(
+        &self,
+        counter_data: &str,
+        span: SpanStable,
+        code_region: CodeRegion,
+    ) -> Stmt {
         let loc = self.codegen_caller_span_stable(span);
         // Should use Stmt::cover, but currently this doesn't work with CBMC
         // unless it is run with '--cover cover' (see
         // https://github.com/diffblue/cbmc/issues/6613). So for now use
         // `assert(false)`.
-        self.codegen_assert(
-            Expr::bool_false(),
-            PropertyClass::CodeCoverage,
-            "code coverage for location",
-            loc,
-        )
+        let msg = format!("{counter_data} - {code_region:?}");
+        self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc)
     }
 
     // The above represent the basic operations we can perform w.r.t. assert/assume/cover
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
index 5fe28097a2e0..1b28de887002 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
@@ -20,53 +20,24 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) {
         debug!(?bb, "codegen_block");
         let label = bb_label(bb);
-        let check_coverage = self.queries.args().check_coverage;
         // the first statement should be labelled. if there is no statements, then the
         // terminator should be labelled.
         match bbd.statements.len() {
             0 => {
                 let term = &bbd.terminator;
                 let tcode = self.codegen_terminator(term);
-                // When checking coverage, the `coverage` check should be
-                // labelled instead.
-                if check_coverage {
-                    let span = term.span;
-                    let cover = self.codegen_coverage(span);
-                    self.current_fn_mut().push_onto_block(cover.with_label(label));
-                    self.current_fn_mut().push_onto_block(tcode);
-                } else {
-                    self.current_fn_mut().push_onto_block(tcode.with_label(label));
-                }
+                self.current_fn_mut().push_onto_block(tcode.with_label(label));
             }
             _ => {
                 let stmt = &bbd.statements[0];
                 let scode = self.codegen_statement(stmt);
-                // When checking coverage, the `coverage` check should be
-                // labelled instead.
-                if check_coverage {
-                    let span = stmt.span;
-                    let cover = self.codegen_coverage(span);
-                    self.current_fn_mut().push_onto_block(cover.with_label(label));
-                    self.current_fn_mut().push_onto_block(scode);
-                } else {
-                    self.current_fn_mut().push_onto_block(scode.with_label(label));
-                }
+                self.current_fn_mut().push_onto_block(scode.with_label(label));
 
                 for s in &bbd.statements[1..] {
-                    if check_coverage {
-                        let span = s.span;
-                        let cover = self.codegen_coverage(span);
-                        self.current_fn_mut().push_onto_block(cover);
-                    }
                     let stmt = self.codegen_statement(s);
                     self.current_fn_mut().push_onto_block(stmt);
                 }
                 let term = &bbd.terminator;
-                if check_coverage {
-                    let span = term.span;
-                    let cover = self.codegen_coverage(span);
-                    self.current_fn_mut().push_onto_block(cover);
-                }
                 let tcode = self.codegen_terminator(term);
                 self.current_fn_mut().push_onto_block(tcode);
             }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index a1afa343a6e7..0793e0c4688f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -216,3 +216,74 @@ impl<'tcx> GotocCtx<'tcx> {
         self.reset_current_fn();
     }
 }
+
+pub mod rustc_smir {
+    use crate::stable_mir::CrateDef;
+    use rustc_middle::mir::coverage::CodeRegion;
+    use rustc_middle::mir::coverage::CovTerm;
+    use rustc_middle::mir::coverage::MappingKind::Code;
+    use rustc_middle::ty::TyCtxt;
+    use stable_mir::mir::mono::Instance;
+    use stable_mir::Opaque;
+
+    type CoverageOpaque = stable_mir::Opaque;
+
+    /// Retrieves the `CodeRegion` associated with the data in a
+    /// `CoverageOpaque` object.
+    pub fn region_from_coverage_opaque(
+        tcx: TyCtxt,
+        coverage_opaque: &CoverageOpaque,
+        instance: Instance,
+    ) -> Option<CodeRegion> {
+        let cov_term = parse_coverage_opaque(coverage_opaque);
+        region_from_coverage(tcx, cov_term, instance)
+    }
+
+    /// Retrieves the `CodeRegion` associated with a `CovTerm` object.
+    ///
+    /// Note: This function could be in the internal `rustc` impl for `Coverage`.
+    pub fn region_from_coverage(
+        tcx: TyCtxt<'_>,
+        coverage: CovTerm,
+        instance: Instance,
+    ) -> Option<CodeRegion> {
+        // We need to pull the coverage info from the internal MIR instance.
+        let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
+        let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
+
+        // Some functions, like `std` ones, may not have coverage info attached
+        // to them because they have been compiled without coverage flags.
+        if let Some(cov_info) = &body.function_coverage_info {
+            // Iterate over the coverage mappings and match with the coverage term.
+            for mapping in &cov_info.mappings {
+                let Code(term) = mapping.kind else { unreachable!() };
+                if term == coverage {
+                    return Some(mapping.code_region.clone());
+                }
+            }
+        }
+        None
+    }
+
+    /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`:
+    /// <https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CovTerm.html>
+    ///
+    /// At present, a `CovTerm` can be one of the following:
+    ///  - `CounterIncrement(<num>)`: A physical counter.
+    ///  - `ExpressionUsed(<num>)`: An expression-based counter.
+    ///  - `Zero`: A counter with a constant zero value.
+    fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm {
+        let coverage_str = coverage_opaque.to_string();
+        if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") {
+            let (num_str, _rest) = rest.split_once(')').unwrap();
+            let num = num_str.parse::<u32>().unwrap();
+            CovTerm::Counter(num.into())
+        } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") {
+            let (num_str, _rest) = rest.split_once(')').unwrap();
+            let num = num_str.parse::<u32>().unwrap();
+            CovTerm::Expression(num.into())
+        } else {
+            CovTerm::Zero
+        }
+    }
+}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index b8db1a3d52b6..81407c4dc704 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -3,6 +3,7 @@
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
 use super::{bb_label, PropertyClass};
+use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
@@ -158,12 +159,28 @@ impl<'tcx> GotocCtx<'tcx> {
                     location,
                 )
             }
+            StatementKind::Coverage(coverage_opaque) => {
+                let function_name = self.current_fn().readable_name();
+                let instance = self.current_fn().instance_stable();
+                let counter_data = format!("{coverage_opaque:?} ${function_name}$");
+                let maybe_code_region =
+                    region_from_coverage_opaque(self.tcx, &coverage_opaque, instance);
+                if let Some(code_region) = maybe_code_region {
+                    let coverage_stmt =
+                        self.codegen_coverage(&counter_data, stmt.span, code_region);
+                    // TODO: Avoid single-statement blocks when conversion of
+                    // standalone statements to the irep format is fixed.
+                    // More details in <https://github.com/model-checking/kani/issues/3012>
+                    Stmt::block(vec![coverage_stmt], location)
+                } else {
+                    Stmt::skip(location)
+                }
+            }
             StatementKind::PlaceMention(_) => todo!(),
             StatementKind::FakeRead(..)
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType { .. }
             | StatementKind::Nop
-            | StatementKind::Coverage { .. }
             | StatementKind::ConstEvalCounter => Stmt::skip(location),
         }
         .with_location(location)
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index c57ec8e8e2f2..27fef66ffb65 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -34,6 +34,7 @@ tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_de
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
 rand = "0.8"
 which = "6"
+time = {version = "0.3.36", features = ["formatting"]}
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 2d7593e8050a..c3cfc113af64 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -615,12 +615,12 @@ impl ValidateArgs for VerificationArgs {
         }
 
         if self.coverage
-            && !self.common_args.unstable_features.contains(UnstableFeature::LineCoverage)
+            && !self.common_args.unstable_features.contains(UnstableFeature::SourceCoverage)
         {
             return Err(Error::raw(
                 ErrorKind::MissingRequiredArgument,
                 "The `--coverage` argument is unstable and requires `-Z \
-            line-coverage` to be used.",
+            source-coverage` to be used.",
             ));
         }
 
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 4e8e83b562af..e69062a0cd4f 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -206,7 +206,7 @@ impl KaniSession {
         })
     }
 
-    fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
+    pub fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
         let mut cmd = MetadataCommand::new();
 
         // restrict metadata command to host platform. References:
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 387a9723fcdb..bc4424aeb231 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -3,10 +3,15 @@
 
 use anyhow::{bail, Result};
 use kani_metadata::{CbmcSolver, HarnessMetadata};
+use regex::Regex;
+use rustc_demangle::demangle;
+use std::collections::btree_map::Entry;
+use std::collections::BTreeMap;
 use std::ffi::OsString;
 use std::fmt::Write;
 use std::path::Path;
 use std::process::Command;
+use std::sync::OnceLock;
 use std::time::{Duration, Instant};
 
 use crate::args::{OutputFormat, VerificationArgs};
@@ -14,6 +19,8 @@ use crate::cbmc_output_parser::{
     extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput,
 };
 use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
+use crate::coverage::cov_results::{CoverageCheck, CoverageResults};
+use crate::coverage::cov_results::{CoverageRegion, CoverageTerm};
 use crate::session::KaniSession;
 
 /// We will use Cadical by default since it performed better than MiniSAT in our analysis.
@@ -54,6 +61,8 @@ pub struct VerificationResult {
     pub runtime: Duration,
     /// Whether concrete playback generated a test
     pub generated_concrete_test: bool,
+    /// The coverage results
+    pub coverage_results: Option<CoverageResults>,
 }
 
 impl KaniSession {
@@ -273,12 +282,14 @@ impl VerificationResult {
         if let Some(results) = results {
             let (status, failed_properties) =
                 verification_outcome_from_properties(&results, should_panic);
+            let coverage_results = coverage_results_from_properties(&results);
             VerificationResult {
                 status,
                 failed_properties,
                 results: Ok(results),
                 runtime,
                 generated_concrete_test: false,
+                coverage_results,
             }
         } else {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
@@ -288,6 +299,7 @@ impl VerificationResult {
                 results: Err(output.process_status),
                 runtime,
                 generated_concrete_test: false,
+                coverage_results: None,
             }
         }
     }
@@ -299,6 +311,7 @@ impl VerificationResult {
             results: Ok(vec![]),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
+            coverage_results: None,
         }
     }
 
@@ -312,23 +325,26 @@ impl VerificationResult {
             results: Err(42),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
+            coverage_results: None,
         }
     }
 
-    pub fn render(
-        &self,
-        output_format: &OutputFormat,
-        should_panic: bool,
-        coverage_mode: bool,
-    ) -> String {
+    pub fn render(&self, output_format: &OutputFormat, should_panic: bool) -> String {
         match &self.results {
             Ok(results) => {
                 let status = self.status;
                 let failed_properties = self.failed_properties;
                 let show_checks = matches!(output_format, OutputFormat::Regular);
 
-                let mut result = if coverage_mode {
-                    format_coverage(results, status, should_panic, failed_properties, show_checks)
+                let mut result = if let Some(cov_results) = &self.coverage_results {
+                    format_coverage(
+                        results,
+                        cov_results,
+                        status,
+                        should_panic,
+                        failed_properties,
+                        show_checks,
+                    )
                 } else {
                     format_result(results, status, should_panic, failed_properties, show_checks)
                 };
@@ -404,6 +420,74 @@ fn determine_failed_properties(properties: &[Property]) -> FailedProperties {
     }
 }
 
+fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageResults> {
+    let cov_properties: Vec<&Property> =
+        properties.iter().filter(|p| p.is_code_coverage_property()).collect();
+
+    if cov_properties.is_empty() {
+        return None;
+    }
+
+    // Postprocessing the coverage results involves matching on the descriptions
+    // of code coverage properties with the `counter_re` regex. These are two
+    // real examples of such descriptions:
+    //
+    // ```
+    // CounterIncrement(0) $test_cov$ - src/main.rs:5:1 - 6:15
+    // ExpressionUsed(0) $test_cov$ - src/main.rs:6:19 - 6:28
+    // ```
+    //
+    // The span is further processed to extract the code region attributes.
+    // Ideally, we should have coverage mappings (i.e., the relation between
+    // counters and code regions) available in the coverage metadata:
+    // <https://github.com/model-checking/kani/issues/3445>. If that were the
+    // case, we would not need the spans in these descriptions.
+    let counter_re = {
+        static COUNTER_RE: OnceLock<Regex> = OnceLock::new();
+        COUNTER_RE.get_or_init(|| {
+            Regex::new(
+                r#"^(?<kind>CounterIncrement|ExpressionUsed)\((?<counter_num>[0-9]+)\) \$(?<func_name>[^\$]+)\$ - (?<span>.+)"#,
+            )
+            .unwrap()
+        })
+    };
+
+    let mut coverage_results: BTreeMap<String, Vec<CoverageCheck>> = BTreeMap::default();
+
+    for prop in cov_properties {
+        let mut prop_processed = false;
+
+        if let Some(captures) = counter_re.captures(&prop.description) {
+            let kind = &captures["kind"];
+            let counter_num = &captures["counter_num"];
+            let function = demangle(&captures["func_name"]).to_string();
+            let status = prop.status;
+            let span = captures["span"].to_string();
+
+            let counter_id = counter_num.parse().unwrap();
+            let term = match kind {
+                "CounterIncrement" => CoverageTerm::Counter(counter_id),
+                "ExpressionUsed" => CoverageTerm::Expression(counter_id),
+                _ => unreachable!("counter kind could not be recognized: {:?}", kind),
+            };
+            let region = CoverageRegion::from_str(span);
+
+            let cov_check = CoverageCheck::new(function, term, region, status);
+            let file = cov_check.region.file.clone();
+
+            if let Entry::Vacant(e) = coverage_results.entry(file.clone()) {
+                e.insert(vec![cov_check]);
+            } else {
+                coverage_results.entry(file).and_modify(|checks| checks.push(cov_check));
+            }
+            prop_processed = true;
+        }
+
+        assert!(prop_processed, "error: coverage property not processed\n{prop:?}");
+    }
+
+    Some(CoverageResults::new(coverage_results))
+}
 /// 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/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 4b30fe877507..868d1adce636 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -155,6 +155,11 @@ impl KaniSession {
     pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec<OsString> {
         let mut flags: Vec<_> = base_rustc_flags(lib_config);
         // We only use panic abort strategy for verification since we cannot handle unwind logic.
+        if self.args.coverage {
+            flags.extend_from_slice(
+                &["-C", "instrument-coverage", "-Z", "no-profiler-runtime"].map(OsString::from),
+            );
+        }
         flags.extend_from_slice(
             &[
                 "-C",
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index b3a78e8d03e2..8ef1ee153106 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -27,7 +27,7 @@ use anyhow::Result;
 use console::style;
 use pathdiff::diff_paths;
 use rustc_demangle::demangle;
-use serde::{Deserialize, Deserializer};
+use serde::{Deserialize, Deserializer, Serialize};
 
 use std::env;
 use std::io::{BufRead, BufReader};
@@ -321,7 +321,7 @@ impl std::fmt::Display for TraceData {
     }
 }
 
-#[derive(Copy, Clone, Debug, Deserialize, PartialEq, Eq)]
+#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
 #[serde(rename_all = "UPPERCASE")]
 pub enum CheckStatus {
     Failure,
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index 4f32028b5866..a0202169863c 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -4,12 +4,12 @@
 use crate::args::OutputFormat;
 use crate::call_cbmc::{FailedProperties, VerificationStatus};
 use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem};
+use crate::coverage::cov_results::CoverageResults;
 use console::style;
 use once_cell::sync::Lazy;
 use regex::Regex;
 use rustc_demangle::demangle;
-use std::collections::{BTreeMap, HashMap};
-use strum_macros::{AsRefStr, Display};
+use std::collections::HashMap;
 
 type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>;
 
@@ -150,15 +150,6 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
     map
 });
 
-#[derive(PartialEq, Eq, AsRefStr, Clone, Copy, Display)]
-#[strum(serialize_all = "UPPERCASE")]
-// The status of coverage reported by Kani
-enum CoverageStatus {
-    Full,
-    Partial,
-    None,
-}
-
 const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani";
 const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop";
 const UNWINDING_ASSERT_REC_DESC: &str = "recursion unwinding assertion";
@@ -431,72 +422,31 @@ pub fn format_result(
     result_str
 }
 
-/// Separate checks into coverage and non-coverage based on property class and format them separately for --coverage. We report both verification and processed coverage
-/// results
+/// Separate checks into coverage and non-coverage based on property class and
+/// format them separately for `--coverage`. Then we report both verification
+/// and processed coverage results.
+///
+/// Note: The reporting of coverage results should be removed once `kani-cov` is
+/// introduced.
 pub fn format_coverage(
     properties: &[Property],
+    cov_results: &CoverageResults,
     status: VerificationStatus,
     should_panic: bool,
     failed_properties: FailedProperties,
     show_checks: bool,
 ) -> String {
-    let (coverage_checks, non_coverage_checks): (Vec<Property>, Vec<Property>) =
+    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);
-    let coverage_output = format_result_coverage(&coverage_checks);
-    let result = format!("{}\n{}", verification_output, coverage_output);
+    let cov_results_intro = "Source-based code coverage results:";
+    let result = format!("{}\n{}\n\n{}", verification_output, cov_results_intro, cov_results);
 
     result
 }
 
-/// Generate coverage result from all coverage properties (i.e., checks with `code_coverage` property class).
-/// Loops through each of the checks with the `code_coverage` property class on a line and gives:
-///  - A status `FULL` if all checks pertaining to a line number are `COVERED`
-///  - A status `NONE` if all checks related to a line are `UNCOVERED`
-///  - Otherwise (i.e., if the line contains both) it reports `PARTIAL`.
-///
-/// Used when the user requests coverage information with `--coverage`.
-/// Output is tested through the `coverage-based` testing suite, not the regular
-/// `expected` suite.
-fn format_result_coverage(properties: &[Property]) -> String {
-    let mut formatted_output = String::new();
-    formatted_output.push_str("\nCoverage Results:\n");
-
-    let mut coverage_results: BTreeMap<String, BTreeMap<usize, CoverageStatus>> =
-        BTreeMap::default();
-    for prop in properties {
-        let src = prop.source_location.clone();
-        let file_entries = coverage_results.entry(src.file.unwrap()).or_default();
-        let check_status = if prop.status == CheckStatus::Covered {
-            CoverageStatus::Full
-        } else {
-            CoverageStatus::None
-        };
-
-        // Create Map<file, Map<line, status>>
-        file_entries
-            .entry(src.line.unwrap().parse().unwrap())
-            .and_modify(|line_status| {
-                if *line_status != check_status {
-                    *line_status = CoverageStatus::Partial
-                }
-            })
-            .or_insert(check_status);
-    }
-
-    // Create formatted string that is returned to the user as output
-    for (file, checks) in coverage_results.iter() {
-        for (line_number, coverage_status) in checks {
-            formatted_output.push_str(&format!("{}, {}, {}\n", file, line_number, coverage_status));
-        }
-        formatted_output.push('\n');
-    }
-
-    formatted_output
-}
-
 /// Attempts to build a message for a failed property with as much detailed
 /// information on the source location as possible.
 fn build_failure_message(description: String, trace: &Option<Vec<TraceItem>>) -> String {
diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs
new file mode 100644
index 000000000000..845ae7de21bb
--- /dev/null
+++ b/kani-driver/src/coverage/cov_results.rs
@@ -0,0 +1,96 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::cbmc_output_parser::CheckStatus;
+use serde::{Deserialize, Serialize};
+use std::{collections::BTreeMap, fmt, fmt::Display};
+
+/// The coverage data maps a function name to a set of coverage checks.
+#[derive(Clone, Debug, Serialize, Deserialize)]
+pub struct CoverageResults {
+    pub data: BTreeMap<String, Vec<CoverageCheck>>,
+}
+
+impl CoverageResults {
+    pub fn new(data: BTreeMap<String, Vec<CoverageCheck>>) -> Self {
+        Self { data }
+    }
+}
+
+impl fmt::Display for CoverageResults {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        for (file, checks) in self.data.iter() {
+            let mut checks_by_function: BTreeMap<String, Vec<CoverageCheck>> = BTreeMap::new();
+
+            // Group checks by function
+            for check in checks {
+                // Insert the check into the vector corresponding to its function
+                checks_by_function.entry(check.function.clone()).or_default().push(check.clone());
+            }
+
+            for (function, checks) in checks_by_function {
+                writeln!(f, "{file} ({function})")?;
+                let mut sorted_checks: Vec<CoverageCheck> = checks.to_vec();
+                sorted_checks.sort_by(|a, b| a.region.start.cmp(&b.region.start));
+                for check in sorted_checks.iter() {
+                    writeln!(f, " * {} {}", check.region, check.status)?;
+                }
+                writeln!(f)?;
+            }
+        }
+        Ok(())
+    }
+}
+
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct CoverageCheck {
+    pub function: String,
+    term: CoverageTerm,
+    pub region: CoverageRegion,
+    status: CheckStatus,
+}
+
+impl CoverageCheck {
+    pub fn new(
+        function: String,
+        term: CoverageTerm,
+        region: CoverageRegion,
+        status: CheckStatus,
+    ) -> Self {
+        Self { function, term, region, status }
+    }
+}
+
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub enum CoverageTerm {
+    Counter(u32),
+    Expression(u32),
+}
+
+#[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)]
+pub struct CoverageRegion {
+    pub file: String,
+    pub start: (u32, u32),
+    pub end: (u32, u32),
+}
+
+impl Display for CoverageRegion {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}:{} - {}:{}", self.start.0, self.start.1, self.end.0, self.end.1)
+    }
+}
+
+impl CoverageRegion {
+    pub fn from_str(str: String) -> Self {
+        let blank_splits: Vec<&str> = str.split_whitespace().map(|s| s.trim()).collect();
+        assert!(blank_splits[1] == "-");
+        let str_splits1: Vec<&str> = blank_splits[0].split([':']).collect();
+        let str_splits2: Vec<&str> = blank_splits[2].split([':']).collect();
+        assert_eq!(str_splits1.len(), 3, "{str:?}");
+        assert_eq!(str_splits2.len(), 2, "{str:?}");
+        let file = str_splits1[0].to_string();
+        let start = (str_splits1[1].parse().unwrap(), str_splits1[2].parse().unwrap());
+        let end = (str_splits2[0].parse().unwrap(), str_splits2[1].parse().unwrap());
+        Self { file, start, end }
+    }
+}
diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs
new file mode 100644
index 000000000000..df82d982bd72
--- /dev/null
+++ b/kani-driver/src/coverage/cov_session.rs
@@ -0,0 +1,176 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use std::fs;
+use std::fs::File;
+use std::io::Write;
+
+use crate::harness_runner::HarnessResult;
+use crate::project::Project;
+use crate::KaniSession;
+use anyhow::{bail, Result};
+
+impl KaniSession {
+    /// Saves metadata required for coverage-related features.
+    /// At present, this metadata consists of the following:
+    ///  - The file names of the project's source code.
+    ///
+    /// Note: Currently, coverage mappings are not included due to technical
+    /// limitations. But this is where we should save them.
+    pub fn save_coverage_metadata(&self, project: &Project, stamp: &String) -> Result<()> {
+        if self.args.target_dir.is_some() {
+            self.save_coverage_metadata_cargo(project, stamp)
+        } else {
+            self.save_coverage_metadata_standalone(project, stamp)
+        }
+    }
+
+    fn save_coverage_metadata_cargo(&self, project: &Project, stamp: &String) -> Result<()> {
+        let build_target = env!("TARGET");
+        let metadata = self.cargo_metadata(build_target)?;
+        let target_dir = self
+            .args
+            .target_dir
+            .as_ref()
+            .unwrap_or(&metadata.target_directory.clone().into())
+            .clone()
+            .join("kani");
+
+        let outdir = target_dir.join(build_target).join(format!("kanicov_{stamp}"));
+
+        // Generally we don't expect this directory to exist, but there's no
+        // reason to delete it if it does.
+        if !outdir.exists() {
+            fs::create_dir(&outdir)?;
+        }
+
+        // Collect paths to source files in the project
+        let mut source_targets = Vec::new();
+        if let Some(metadata) = &project.cargo_metadata {
+            for package in &metadata.packages {
+                for target in &package.targets {
+                    source_targets.push(target.src_path.clone());
+                }
+            }
+        } else {
+            bail!("could not find project metadata required for coverage metadata");
+        }
+
+        let kanimap_name = format!("kanicov_{stamp}_kanimap");
+        let file_name = outdir.join(kanimap_name).with_extension("json");
+        let mut kanimap_file = File::create(file_name)?;
+
+        let serialized_data = serde_json::to_string(&source_targets)?;
+        kanimap_file.write_all(serialized_data.as_bytes())?;
+
+        Ok(())
+    }
+
+    fn save_coverage_metadata_standalone(&self, project: &Project, stamp: &String) -> Result<()> {
+        let input = project.input.clone().unwrap().canonicalize().unwrap();
+        let input_dir = input.parent().unwrap().to_path_buf();
+        let outdir = input_dir.join(format!("kanicov_{stamp}"));
+
+        // Generally we don't expect this directory to exist, but there's no
+        // reason to delete it if it does.
+        if !outdir.exists() {
+            fs::create_dir(&outdir)?;
+        }
+
+        // In this case, the source files correspond to the input file
+        let source_targets = vec![input];
+
+        let kanimap_name = format!("kanicov_{stamp}_kanimap");
+        let file_name = outdir.join(kanimap_name).with_extension("json");
+        let mut kanimap_file = File::create(file_name)?;
+
+        let serialized_data = serde_json::to_string(&source_targets)?;
+        kanimap_file.write_all(serialized_data.as_bytes())?;
+
+        Ok(())
+    }
+
+    /// Saves raw coverage check results required for coverage-related features.
+    pub fn save_coverage_results(
+        &self,
+        project: &Project,
+        results: &Vec<HarnessResult>,
+        stamp: &String,
+    ) -> Result<()> {
+        if self.args.target_dir.is_some() {
+            self.save_coverage_results_cargo(results, stamp)
+        } else {
+            self.save_coverage_results_standalone(project, results, stamp)
+        }
+    }
+
+    pub fn save_coverage_results_cargo(
+        &self,
+        results: &Vec<HarnessResult>,
+        stamp: &String,
+    ) -> Result<()> {
+        let build_target = env!("TARGET");
+        let metadata = self.cargo_metadata(build_target)?;
+        let target_dir = self
+            .args
+            .target_dir
+            .as_ref()
+            .unwrap_or(&metadata.target_directory.clone().into())
+            .clone()
+            .join("kani");
+
+        let outdir = target_dir.join(build_target).join(format!("kanicov_{stamp}"));
+
+        // This directory should have been created by `save_coverage_metadata`,
+        // so now we expect it to exist.
+        if !outdir.exists() {
+            bail!("directory associated to coverage run does not exist")
+        }
+
+        for harness_res in results {
+            let harness_name = harness_res.harness.mangled_name.clone();
+            let kaniraw_name = format!("{harness_name}_kaniraw");
+            let file_name = outdir.join(kaniraw_name).with_extension("json");
+            let mut cov_file = File::create(file_name)?;
+
+            let cov_results = &harness_res.result.coverage_results.clone().unwrap();
+            let serialized_data = serde_json::to_string(&cov_results)?;
+            cov_file.write_all(serialized_data.as_bytes())?;
+        }
+
+        println!("[info] Coverage results saved to {}", &outdir.display());
+        Ok(())
+    }
+
+    pub fn save_coverage_results_standalone(
+        &self,
+        project: &Project,
+        results: &Vec<HarnessResult>,
+        stamp: &String,
+    ) -> Result<()> {
+        let input = project.input.clone().unwrap().canonicalize().unwrap();
+        let input_dir = input.parent().unwrap().to_path_buf();
+        let outdir = input_dir.join(format!("kanicov_{stamp}"));
+
+        // This directory should have been created by `save_coverage_metadata`,
+        // so now we expect it to exist.
+        if !outdir.exists() {
+            bail!("directory associated to coverage run does not exist")
+        }
+
+        for harness_res in results {
+            let harness_name = harness_res.harness.mangled_name.clone();
+            let kaniraw_name = format!("{harness_name}_kaniraw");
+            let file_name = outdir.join(kaniraw_name).with_extension("json");
+            let mut cov_file = File::create(file_name)?;
+
+            let cov_results = &harness_res.result.coverage_results.clone().unwrap();
+            let serialized_data = serde_json::to_string(&cov_results)?;
+            cov_file.write_all(serialized_data.as_bytes())?;
+        }
+
+        println!("[info] Coverage results saved to {}", &outdir.display());
+
+        Ok(())
+    }
+}
diff --git a/kani-driver/src/coverage/mod.rs b/kani-driver/src/coverage/mod.rs
new file mode 100644
index 000000000000..2f7072aa82aa
--- /dev/null
+++ b/kani-driver/src/coverage/mod.rs
@@ -0,0 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub mod cov_results;
+pub mod cov_session;
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 992e226e45db..7e432932ab29 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -124,11 +124,7 @@ impl KaniSession {
             if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
                 println!(
                     "{}",
-                    result.render(
-                        &self.args.output_format,
-                        harness.attributes.should_panic,
-                        self.args.coverage
-                    )
+                    result.render(&self.args.output_format, harness.attributes.should_panic)
                 );
             }
             self.gen_and_add_concrete_playback(harness, &mut result)?;
@@ -192,6 +188,10 @@ impl KaniSession {
             }
         }
 
+        if self.args.coverage {
+            self.show_coverage_summary()?;
+        }
+
         if failing > 0 {
             // Failure exit code without additional error message
             drop(self);
@@ -200,4 +200,11 @@ impl KaniSession {
 
         Ok(())
     }
+
+    /// Show a coverage summary.
+    ///
+    /// This is just a placeholder for now.
+    fn show_coverage_summary(&self) -> Result<()> {
+        Ok(())
+    }
 }
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 3bb38ed1294c..d3bd697d2ea4 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -5,6 +5,7 @@ use std::ffi::OsString;
 use std::process::ExitCode;
 
 use anyhow::Result;
+use time::{format_description, OffsetDateTime};
 
 use args::{check_is_valid, CargoKaniSubcommand};
 use args_toml::join_args;
@@ -30,6 +31,7 @@ mod call_single_file;
 mod cbmc_output_parser;
 mod cbmc_property_renderer;
 mod concrete_playback;
+mod coverage;
 mod harness_runner;
 mod metadata;
 mod project;
@@ -129,6 +131,23 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
     let runner = harness_runner::HarnessRunner { sess: &session, project: &project };
     let results = runner.check_all_harnesses(&harnesses)?;
 
+    if session.args.coverage {
+        // We generate a timestamp to save the coverage data in a folder named
+        // `kanicov_<date>` where `<date>` is the current date based on `format`
+        // below. The purpose of adding timestamps to the folder name is to make
+        // coverage results easily identifiable. Using a timestamp makes
+        // coverage results not only distinguishable, but also easy to relate to
+        // verification runs. We expect this to be particularly helpful for
+        // users in a proof debugging session, who are usually interested in the
+        // most recent results.
+        let time_now = OffsetDateTime::now_utc();
+        let format = format_description::parse("[year]-[month]-[day]_[hour]-[minute]").unwrap();
+        let timestamp = time_now.format(&format).unwrap();
+
+        session.save_coverage_metadata(&project, &timestamp)?;
+        session.save_coverage_results(&project, &results, &timestamp)?;
+    }
+
     session.print_final_summary(&results)
 }
 
diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
index 2bc0845cdb46..e0d2d2edd139 100644
--- a/kani-driver/src/project.rs
+++ b/kani-driver/src/project.rs
@@ -33,6 +33,9 @@ pub struct Project {
     /// The directory where all outputs should be directed to. This path represents the canonical
     /// version of outdir.
     pub outdir: PathBuf,
+    /// The path to the input file the project was built from.
+    /// Note that it will only be `Some(...)` if this was built from a standalone project.
+    pub input: Option<PathBuf>,
     /// The collection of artifacts kept as part of this project.
     artifacts: Vec<Artifact>,
     /// Records the cargo metadata from the build, if there was any
@@ -82,6 +85,7 @@ impl Project {
     fn try_new(
         session: &KaniSession,
         outdir: PathBuf,
+        input: Option<PathBuf>,
         metadata: Vec<KaniMetadata>,
         cargo_metadata: Option<cargo_metadata::Metadata>,
         failed_targets: Option<Vec<String>>,
@@ -115,7 +119,7 @@ impl Project {
             }
         }
 
-        Ok(Project { outdir, metadata, artifacts, cargo_metadata, failed_targets })
+        Ok(Project { outdir, input, metadata, artifacts, cargo_metadata, failed_targets })
     }
 }
 
@@ -178,6 +182,7 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result<Project>
     Project::try_new(
         session,
         outdir,
+        None,
         metadata,
         Some(outputs.cargo_metadata),
         outputs.failed_targets,
@@ -243,7 +248,14 @@ impl<'a> StandaloneProjectBuilder<'a> {
         let metadata = from_json(&self.metadata)?;
 
         // Create the project with the artifacts built by the compiler.
-        let result = Project::try_new(self.session, self.outdir, vec![metadata], None, None);
+        let result = Project::try_new(
+            self.session,
+            self.outdir,
+            Some(self.input),
+            vec![metadata],
+            None,
+            None,
+        );
         if let Ok(project) = &result {
             self.session.record_temporary_files(&project.artifacts);
         }
@@ -297,5 +309,5 @@ pub(crate) fn std_project(std_path: &Path, session: &KaniSession) -> Result<Proj
 
     // Get the metadata and return a Kani project.
     let metadata = outputs.iter().map(|md_file| from_json(md_file)).collect::<Result<Vec<_>>>()?;
-    Project::try_new(session, outdir, metadata, None, None)
+    Project::try_new(session, outdir, None, metadata, None, None)
 }
diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs
index 120ab0a9e55c..11df998c820f 100644
--- a/kani_metadata/src/unstable.rs
+++ b/kani_metadata/src/unstable.rs
@@ -78,8 +78,9 @@ pub enum UnstableFeature {
     ConcretePlayback,
     /// Enable Kani's unstable async library.
     AsyncLib,
-    /// Enable line coverage instrumentation/reports.
-    LineCoverage,
+    /// Enable source-based code coverage workflow.
+    /// See [RFC-0011](https://model-checking.github.io/kani/rfc/rfcs/0011-source-coverage.html)
+    SourceCoverage,
     /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html)
     FunctionContracts,
     /// Memory predicate APIs.
diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected
new file mode 100644
index 000000000000..91142ebf94fc
--- /dev/null
+++ b/tests/coverage/abort/expected
@@ -0,0 +1,13 @@
+Source-based code coverage results:
+
+main.rs (main)\
+ * 9:1 - 9:11 COVERED\
+ * 10:9 - 10:10 COVERED\
+ * 10:14 - 10:18 COVERED\
+ * 13:13 - 13:29 COVERED\
+ * 14:10 - 15:18 COVERED\
+ * 17:13 - 17:29 UNCOVERED\
+ * 18:10 - 18:11 COVERED\
+ * 20:5 - 20:12 UNCOVERED\
+ * 20:20 - 20:41 UNCOVERED\
+ * 21:1 - 21:2 UNCOVERED
diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/abort/main.rs
similarity index 100%
rename from tests/coverage/unreachable/abort/main.rs
rename to tests/coverage/abort/main.rs
diff --git a/tests/coverage/assert/expected b/tests/coverage/assert/expected
new file mode 100644
index 000000000000..46bb664cf6f5
--- /dev/null
+++ b/tests/coverage/assert/expected
@@ -0,0 +1,9 @@
+Source-based code coverage results:
+
+test.rs (foo)
+ * 5:1 - 7:13 COVERED\
+ * 9:9 - 10:17 COVERED\
+ * 10:18 - 13:10 UNCOVERED\
+ * 13:10 - 13:11 UNCOVERED\
+ * 14:12 - 17:6 COVERED\
+ * 18:1 - 18:2 COVERED
diff --git a/tests/coverage/unreachable/assert/test.rs b/tests/coverage/assert/test.rs
similarity index 100%
rename from tests/coverage/unreachable/assert/test.rs
rename to tests/coverage/assert/test.rs
diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected
new file mode 100644
index 000000000000..c2eee7adf803
--- /dev/null
+++ b/tests/coverage/assert_eq/expected
@@ -0,0 +1,8 @@
+Source-based code coverage results:
+
+test.rs (main)\
+ * 5:1 - 6:29 COVERED\
+ * 7:25 - 7:27 COVERED\
+ * 7:37 - 7:39 COVERED\
+ * 8:15 - 10:6 UNCOVERED\
+ * 10:6 - 10:7 COVERED
diff --git a/tests/coverage/unreachable/assert_eq/test.rs b/tests/coverage/assert_eq/test.rs
similarity index 100%
rename from tests/coverage/unreachable/assert_eq/test.rs
rename to tests/coverage/assert_eq/test.rs
diff --git a/tests/coverage/assert_ne/expected b/tests/coverage/assert_ne/expected
new file mode 100644
index 000000000000..c9b727da0f82
--- /dev/null
+++ b/tests/coverage/assert_ne/expected
@@ -0,0 +1,9 @@
+Source-based code coverage results:
+
+test.rs (main)\
+ * 5:1 - 7:13 COVERED\
+ * 8:13 - 10:18 COVERED\
+ * 10:19 - 12:10 UNCOVERED\
+ * 12:10 - 12:11 COVERED\
+ * 13:6 - 13:7 COVERED\
+ * 14:1 - 14:2 COVERED
diff --git a/tests/coverage/unreachable/assert_ne/test.rs b/tests/coverage/assert_ne/test.rs
similarity index 100%
rename from tests/coverage/unreachable/assert_ne/test.rs
rename to tests/coverage/assert_ne/test.rs
diff --git a/tests/coverage/break/expected b/tests/coverage/break/expected
new file mode 100644
index 000000000000..739735cdf1a2
--- /dev/null
+++ b/tests/coverage/break/expected
@@ -0,0 +1,13 @@
+Source-based code coverage results:
+
+main.rs (find_positive)\
+ * 4:1 - 4:47 COVERED\
+ * 5:10 - 5:13 COVERED\
+ * 5:17 - 5:21 COVERED\
+ * 7:20 - 7:29 COVERED\
+ * 8:10 - 8:11 COVERED\
+ * 11:5 - 11:9 UNCOVERED\
+ * 12:1 - 12:2 COVERED
+
+main.rs (main)\
+ * 15:1 - 19:2 COVERED
diff --git a/tests/coverage/unreachable/break/main.rs b/tests/coverage/break/main.rs
similarity index 82%
rename from tests/coverage/unreachable/break/main.rs
rename to tests/coverage/break/main.rs
index 4e795bd2a6ea..79f422a0c283 100644
--- a/tests/coverage/unreachable/break/main.rs
+++ b/tests/coverage/break/main.rs
@@ -7,7 +7,7 @@ fn find_positive(nums: &[i32]) -> Option<i32> {
             return Some(num);
         }
     }
-    // This part is unreachable if there is at least one positive number.
+    // `None` is unreachable because there is at least one positive number.
     None
 }
 
diff --git a/tests/coverage/compare/expected b/tests/coverage/compare/expected
new file mode 100644
index 000000000000..153dbfa37d80
--- /dev/null
+++ b/tests/coverage/compare/expected
@@ -0,0 +1,11 @@
+Source-based code coverage results:
+
+main.rs (compare)\
+ * 4:1 - 6:14 COVERED\
+ * 6:17 - 6:18 COVERED\
+ * 6:28 - 6:29 UNCOVERED
+
+main.rs (main)\
+ * 10:1 - 13:14 COVERED\
+ * 13:15 - 15:6 COVERED\
+ * 15:6 - 15:7 COVERED
diff --git a/tests/coverage/unreachable/compare/main.rs b/tests/coverage/compare/main.rs
similarity index 73%
rename from tests/coverage/unreachable/compare/main.rs
rename to tests/coverage/compare/main.rs
index a10fb84e29a8..43318ac0547e 100644
--- a/tests/coverage/unreachable/compare/main.rs
+++ b/tests/coverage/compare/main.rs
@@ -2,7 +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
+    // The case where `x < y` isn't possible so its region is `UNCOVERED`
     if x >= y { 1 } else { 0 }
 }
 
diff --git a/tests/coverage/contradiction/expected b/tests/coverage/contradiction/expected
new file mode 100644
index 000000000000..db3676d7da15
--- /dev/null
+++ b/tests/coverage/contradiction/expected
@@ -0,0 +1,9 @@
+Source-based code coverage results:
+
+main.rs (contradiction)\
+ * 4:1 - 7:13 COVERED\
+ * 8:12 - 8:17 COVERED\
+ * 8:18 - 10:10 UNCOVERED\
+ * 10:10 - 10:11 COVERED\
+ * 11:12 - 13:6 COVERED\
+ * 14:1 - 14:2 COVERED
diff --git a/tests/coverage/unreachable/contradiction/main.rs b/tests/coverage/contradiction/main.rs
similarity index 100%
rename from tests/coverage/unreachable/contradiction/main.rs
rename to tests/coverage/contradiction/main.rs
diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected
new file mode 100644
index 000000000000..fbe57690d347
--- /dev/null
+++ b/tests/coverage/debug-assert/expected
@@ -0,0 +1,10 @@
+Source-based code coverage results:
+
+main.rs (main)\
+ * 10:1 - 10:11 COVERED\
+ * 11:9 - 11:10 COVERED\
+ * 11:14 - 11:18 COVERED\
+ * 12:30 - 12:71 UNCOVERED\
+ * 13:9 - 13:23 UNCOVERED\
+ * 13:25 - 13:53 UNCOVERED\
+ * 15:1 - 15:2 UNCOVERED
diff --git a/tests/coverage/debug-assert/main.rs b/tests/coverage/debug-assert/main.rs
new file mode 100644
index 000000000000..a57a45c8c724
--- /dev/null
+++ b/tests/coverage/debug-assert/main.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that the regions after the `debug_assert` macro are
+//! `UNCOVERED`. In fact, for this example, the region associated to `"This
+//! should fail and stop the execution"` is also `UNCOVERED` because the macro
+//! calls span two regions each.
+
+#[kani::proof]
+fn main() {
+    for i in 0..4 {
+        debug_assert!(i > 0, "This should fail and stop the execution");
+        assert!(i == 0, "This should be unreachable");
+    }
+}
diff --git a/tests/coverage/div-zero/expected b/tests/coverage/div-zero/expected
new file mode 100644
index 000000000000..f351005f4f22
--- /dev/null
+++ b/tests/coverage/div-zero/expected
@@ -0,0 +1,9 @@
+Source-based code coverage results:
+
+test.rs (div)\
+ * 4:1 - 5:14 COVERED\
+ * 5:17 - 5:22 COVERED\
+ * 5:32 - 5:33 UNCOVERED
+
+test.rs (main)\
+ * 9:1 - 11:2 COVERED
diff --git a/tests/coverage/reachable/div-zero/reachable_pass/test.rs b/tests/coverage/div-zero/test.rs
similarity index 64%
rename from tests/coverage/reachable/div-zero/reachable_pass/test.rs
rename to tests/coverage/div-zero/test.rs
index 766fb5a89d88..e858b57a12be 100644
--- a/tests/coverage/reachable/div-zero/reachable_pass/test.rs
+++ b/tests/coverage/div-zero/test.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 fn div(x: u16, y: u16) -> u16 {
-    if y != 0 { x / y } else { 0 } // PARTIAL: some cases are `COVERED`, others are not
+    if y != 0 { x / y } else { 0 }
 }
 
 #[kani::proof]
diff --git a/tests/coverage/early-return/expected b/tests/coverage/early-return/expected
new file mode 100644
index 000000000000..53cde3abeaf8
--- /dev/null
+++ b/tests/coverage/early-return/expected
@@ -0,0 +1,12 @@
+Source-based code coverage results:
+
+main.rs (find_index)\
+ * 4:1 - 4:59 COVERED\
+ * 5:10 - 5:21 COVERED\
+ * 7:20 - 7:31 COVERED\
+ * 8:10 - 8:11 COVERED\
+ * 10:5 - 10:9 UNCOVERED\
+ * 11:1 - 11:2 COVERED
+
+main.rs (main)\
+ * 14:1 - 19:2 COVERED
diff --git a/tests/coverage/unreachable/early-return/main.rs b/tests/coverage/early-return/main.rs
similarity index 100%
rename from tests/coverage/unreachable/early-return/main.rs
rename to tests/coverage/early-return/main.rs
diff --git a/tests/coverage/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected
new file mode 100644
index 000000000000..4e8382d10a6f
--- /dev/null
+++ b/tests/coverage/if-statement-multi/expected
@@ -0,0 +1,11 @@
+Source-based code coverage results:
+
+test.rs (main)\
+ * 21:1 - 26:2 COVERED
+
+test.rs (test_cov)\
+ * 16:1 - 17:15 COVERED\
+ * 17:19 - 17:28 UNCOVERED\
+ * 17:31 - 17:35 COVERED\
+ * 17:45 - 17:50 UNCOVERED\
+ * 18:1 - 18:2 COVERED
diff --git a/tests/coverage/if-statement-multi/test.rs b/tests/coverage/if-statement-multi/test.rs
new file mode 100644
index 000000000000..ac00dec3f451
--- /dev/null
+++ b/tests/coverage/if-statement-multi/test.rs
@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --coverage -Zsource-coverage
+
+//! Checks that we are covering all regions except
+//!  * the `val == 42` condition
+//!  * the `false` branch
+//!
+//! No coverage information is shown for `_other_function` because it's sliced
+//! off: <https://github.com/model-checking/kani/issues/3445>
+
+fn _other_function() {
+    println!("Hello, world!");
+}
+
+fn test_cov(val: u32) -> bool {
+    if val < 3 || val == 42 { true } else { false }
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn main() {
+    let test1 = test_cov(1);
+    let test2 = test_cov(2);
+    assert!(test1);
+    assert!(test2);
+}
diff --git a/tests/coverage/if-statement/expected b/tests/coverage/if-statement/expected
new file mode 100644
index 000000000000..b85b95de9c84
--- /dev/null
+++ b/tests/coverage/if-statement/expected
@@ -0,0 +1,14 @@
+Source-based code coverage results:
+
+main.rs (check_number)\
+ * 4:1 - 5:15 COVERED\
+ * 7:12 - 7:24 COVERED\
+ * 7:27 - 7:46 UNCOVERED\
+ * 7:56 - 7:74 COVERED\
+ * 8:15 - 8:22 UNCOVERED\
+ * 9:9 - 9:19 UNCOVERED\
+ * 11:9 - 11:15 UNCOVERED\
+ * 13:1 - 13:2 COVERED
+
+main.rs (main)\
+ * 16:1 - 20:2 COVERED
diff --git a/tests/coverage/unreachable/if-statement/main.rs b/tests/coverage/if-statement/main.rs
similarity index 78%
rename from tests/coverage/unreachable/if-statement/main.rs
rename to tests/coverage/if-statement/main.rs
index f497cd76808e..c18d4dd4a5e4 100644
--- a/tests/coverage/unreachable/if-statement/main.rs
+++ b/tests/coverage/if-statement/main.rs
@@ -3,7 +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
+        // The next line is partially covered
         if num % 2 == 0 { "Positive and Even" } else { "Positive and Odd" }
     } else if num < 0 {
         "Negative"
diff --git a/tests/coverage/known_issues/assert_uncovered_end/expected b/tests/coverage/known_issues/assert_uncovered_end/expected
new file mode 100644
index 000000000000..ceba065ce424
--- /dev/null
+++ b/tests/coverage/known_issues/assert_uncovered_end/expected
@@ -0,0 +1,9 @@
+Source-based code coverage results:
+
+test.rs (check_assert)\
+ * 9:1 - 10:34 COVERED\
+ * 11:14 - 13:6 COVERED\
+ * 13:6 - 13:7 UNCOVERED
+
+test.rs (check_assert::{closure#0})\
+ * 10:40 - 10:49 COVERED
diff --git a/tests/coverage/known_issues/assert_uncovered_end/test.rs b/tests/coverage/known_issues/assert_uncovered_end/test.rs
new file mode 100644
index 000000000000..c3da20c8b00b
--- /dev/null
+++ b/tests/coverage/known_issues/assert_uncovered_end/test.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `check_assert` is fully covered. At present, the coverage for
+//! this test reports an uncovered single-column region at the end of the `if`
+//! statement: <https://github.com/model-checking/kani/issues/3455>
+
+#[kani::proof]
+fn check_assert() {
+    let x: u32 = kani::any_where(|val| *val == 5);
+    if x > 3 {
+        assert!(x > 4);
+    }
+}
diff --git a/tests/coverage/known_issues/assume_assert/expected b/tests/coverage/known_issues/assume_assert/expected
new file mode 100644
index 000000000000..55f3235d7d24
--- /dev/null
+++ b/tests/coverage/known_issues/assume_assert/expected
@@ -0,0 +1,4 @@
+Source-based code coverage results:
+
+main.rs (check_assume_assert)\
+ * 11:1 - 15:2 COVERED
diff --git a/tests/coverage/known_issues/assume_assert/main.rs b/tests/coverage/known_issues/assume_assert/main.rs
new file mode 100644
index 000000000000..90f26b2121fa
--- /dev/null
+++ b/tests/coverage/known_issues/assume_assert/main.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test should check that the region after `kani::assume(false)` is
+//! `UNCOVERED`. However, due to a technical limitation in `rustc`'s coverage
+//! instrumentation, only one `COVERED` region is reported for the whole
+//! function. More details in
+//! <https://github.com/model-checking/kani/issues/3441>.
+
+#[kani::proof]
+fn check_assume_assert() {
+    let a: u8 = kani::any();
+    kani::assume(false);
+    assert!(a < 5);
+}
diff --git a/tests/coverage/known_issues/out-of-bounds/expected b/tests/coverage/known_issues/out-of-bounds/expected
new file mode 100644
index 000000000000..8ab9e2e15627
--- /dev/null
+++ b/tests/coverage/known_issues/out-of-bounds/expected
@@ -0,0 +1,7 @@
+Source-based code coverage results:
+
+test.rs (get)\
+ * 8:1 - 10:2 COVERED
+
+test.rs (main)\
+ * 13:1 - 15:2 COVERED
diff --git a/tests/coverage/known_issues/out-of-bounds/test.rs b/tests/coverage/known_issues/out-of-bounds/test.rs
new file mode 100644
index 000000000000..83242590815b
--- /dev/null
+++ b/tests/coverage/known_issues/out-of-bounds/test.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test should check that the return in `get` is `UNCOVERED`. However, the
+//! coverage results currently report that the whole function is `COVERED`,
+//! likely due to <https://github.com/model-checking/kani/issues/3441>
+
+fn get(s: &[i16], index: usize) -> i16 {
+    s[index]
+}
+
+#[kani::proof]
+fn main() {
+    get(&[7, -83, 19], 15);
+}
diff --git a/tests/coverage/known_issues/variant/expected b/tests/coverage/known_issues/variant/expected
new file mode 100644
index 000000000000..13383ed3bab0
--- /dev/null
+++ b/tests/coverage/known_issues/variant/expected
@@ -0,0 +1,14 @@
+Source-based code coverage results:
+
+main.rs (main)\
+ * 29:1 - 32:2 COVERED
+
+main.rs (print_direction)\
+ * 16:1 - 16:36 COVERED\
+ * 18:11 - 18:14 UNCOVERED\
+ * 19:26 - 19:47 UNCOVERED\
+ * 20:28 - 20:51 UNCOVERED\
+ * 21:28 - 21:51 COVERED\
+ * 22:34 - 22:63 UNCOVERED\
+ * 24:14 - 24:45 UNCOVERED\
+ * 26:1 - 26:2 COVERED
diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/known_issues/variant/main.rs
similarity index 72%
rename from tests/coverage/unreachable/variant/main.rs
rename to tests/coverage/known_issues/variant/main.rs
index 76a589147bca..c654ca355c45 100644
--- a/tests/coverage/unreachable/variant/main.rs
+++ b/tests/coverage/known_issues/variant/main.rs
@@ -2,7 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks coverage results in an example with a `match` statement matching on
-//! all enum variants.
+//! all enum variants. Currently, it does not yield the expected results because
+//! it reports the `dir` in the match statement as `UNCOVERED`:
+//! <https://github.com/model-checking/kani/issues/3456>
 
 enum Direction {
     Up,
@@ -12,6 +14,7 @@ enum Direction {
 }
 
 fn print_direction(dir: Direction) {
+    // For some reason, `dir`'s span is reported as `UNCOVERED` too
     match dir {
         Direction::Up => println!("Going up!"),
         Direction::Down => println!("Going down!"),
diff --git a/tests/coverage/multiple-harnesses/expected b/tests/coverage/multiple-harnesses/expected
new file mode 100644
index 000000000000..b5362147fed1
--- /dev/null
+++ b/tests/coverage/multiple-harnesses/expected
@@ -0,0 +1,37 @@
+Source-based code coverage results:
+
+main.rs (estimate_size)\
+ * 4:1 - 7:15 COVERED\
+ * 8:12 - 8:19 COVERED\
+ * 9:20 - 9:21 COVERED\
+ * 11:20 - 11:21 COVERED\
+ * 13:15 - 13:23 COVERED\
+ * 14:12 - 14:20 COVERED\
+ * 15:20 - 15:21 COVERED\
+ * 17:20 - 17:21 COVERED\
+ * 20:12 - 20:20 COVERED\
+ * 21:20 - 21:21 COVERED\
+ * 23:20 - 23:21 COVERED\
+ * 26:1 - 26:2 COVERED
+
+main.rs (fully_covered)\
+ * 39:1 - 44:2 COVERED
+
+Source-based code coverage results:
+
+main.rs (estimate_size)\
+ * 4:1 - 7:15 COVERED\
+ * 8:12 - 8:19 COVERED\
+ * 9:20 - 9:21 COVERED\
+ * 11:20 - 11:21 COVERED\
+ * 13:15 - 13:23 COVERED\
+ * 14:12 - 14:20 COVERED\
+ * 15:20 - 15:21 COVERED\
+ * 17:20 - 17:21 COVERED\
+ * 20:12 - 20:20 COVERED\
+ * 21:20 - 21:21 COVERED\
+ * 23:20 - 23:21 UNCOVERED\
+ * 26:1 - 26:2 COVERED
+
+main.rs (mostly_covered)\
+ * 30:1 - 35:2 COVERED
diff --git a/tests/coverage/unreachable/multiple-harnesses/main.rs b/tests/coverage/multiple-harnesses/main.rs
similarity index 100%
rename from tests/coverage/unreachable/multiple-harnesses/main.rs
rename to tests/coverage/multiple-harnesses/main.rs
diff --git a/tests/coverage/overflow-failure/expected b/tests/coverage/overflow-failure/expected
new file mode 100644
index 000000000000..db4f29d51336
--- /dev/null
+++ b/tests/coverage/overflow-failure/expected
@@ -0,0 +1,9 @@
+Source-based code coverage results:
+
+test.rs (cond_reduce)\
+ * 7:1 - 8:18 COVERED\
+ * 8:21 - 8:27 COVERED\
+ * 8:37 - 8:38 UNCOVERED
+
+test.rs (main)\
+ * 12:1 - 15:2 COVERED
diff --git a/tests/coverage/reachable/overflow/reachable_fail/test.rs b/tests/coverage/overflow-failure/test.rs
similarity index 66%
rename from tests/coverage/reachable/overflow/reachable_fail/test.rs
rename to tests/coverage/overflow-failure/test.rs
index d435612f2342..cd711f3aeb9e 100644
--- a/tests/coverage/reachable/overflow/reachable_fail/test.rs
+++ b/tests/coverage/overflow-failure/test.rs
@@ -5,11 +5,11 @@
 //! arithmetic overflow failure (caused by the second call to `cond_reduce`).
 
 fn cond_reduce(thresh: u32, x: u32) -> u32 {
-    if x > thresh { x - 50 } else { x } // PARTIAL: some cases are `COVERED`, others are not
+    if x > thresh { x - 50 } else { x }
 }
 
 #[kani::proof]
 fn main() {
     cond_reduce(60, 70);
     cond_reduce(40, 42);
-} // NONE: Caused by the arithmetic overflow failure from the second call to `cond_reduce`
+}
diff --git a/tests/coverage/overflow-full-coverage/expected b/tests/coverage/overflow-full-coverage/expected
new file mode 100644
index 000000000000..4d17761505eb
--- /dev/null
+++ b/tests/coverage/overflow-full-coverage/expected
@@ -0,0 +1,9 @@
+Source-based code coverage results:
+
+test.rs (main)\
+ * 12:1 - 17:2 COVERED
+
+test.rs (reduce)\
+ * 7:1 - 8:16 COVERED\
+ * 8:19 - 8:27 COVERED\
+ * 8:37 - 8:38 COVERED
diff --git a/tests/coverage/reachable/overflow/reachable_pass/test.rs b/tests/coverage/overflow-full-coverage/test.rs
similarity index 62%
rename from tests/coverage/reachable/overflow/reachable_pass/test.rs
rename to tests/coverage/overflow-full-coverage/test.rs
index 0b05874efc84..1c3467275b33 100644
--- a/tests/coverage/reachable/overflow/reachable_pass/test.rs
+++ b/tests/coverage/overflow-full-coverage/test.rs
@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Checks that Kani reports the correct coverage results (`FULL` for all lines)
-//! in a case where arithmetic overflow failures are prevented.
+//! Checks that Kani reports all regions as `COVERED` as expected in this case
+//! where arithmetic overflow failures are prevented.
 
 fn reduce(x: u32) -> u32 {
     if x > 1000 { x - 1000 } else { x }
diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected
deleted file mode 100644
index 97ffbe1d96e4..000000000000
--- a/tests/coverage/reachable/assert-false/expected
+++ /dev/null
@@ -1,8 +0,0 @@
-coverage/reachable/assert-false/main.rs, 6, FULL
-coverage/reachable/assert-false/main.rs, 7, FULL
-coverage/reachable/assert-false/main.rs, 11, PARTIAL
-coverage/reachable/assert-false/main.rs, 12, PARTIAL
-coverage/reachable/assert-false/main.rs, 15, 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
diff --git a/tests/coverage/reachable/assert-false/main.rs b/tests/coverage/reachable/assert-false/main.rs
deleted file mode 100644
index 42563b1cd518..000000000000
--- a/tests/coverage/reachable/assert-false/main.rs
+++ /dev/null
@@ -1,19 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-//! Check that the assert is reported as `PARTIAL` for having both `COVERED` and `UNCOVERED` coverage checks
-fn any_bool() -> bool {
-    kani::any()
-}
-
-#[kani::proof]
-fn main() {
-    if any_bool() {
-        assert!(false);
-    }
-
-    if any_bool() {
-        let s = "Fail with custom runtime message";
-        assert!(false, "{}", s);
-    }
-}
diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected
deleted file mode 100644
index 9d21185b3a83..000000000000
--- a/tests/coverage/reachable/assert/reachable_pass/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/reachable/assert/reachable_pass/test.rs, 6, FULL
-coverage/reachable/assert/reachable_pass/test.rs, 7, PARTIAL
-coverage/reachable/assert/reachable_pass/test.rs, 8, FULL
-coverage/reachable/assert/reachable_pass/test.rs, 10, FULL
diff --git a/tests/coverage/reachable/assert/reachable_pass/test.rs b/tests/coverage/reachable/assert/reachable_pass/test.rs
deleted file mode 100644
index 72acca2b764c..000000000000
--- a/tests/coverage/reachable/assert/reachable_pass/test.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-#[kani::proof]
-fn main() {
-    let x: u32 = kani::any_where(|val| *val == 5);
-    if x > 3 {
-        assert!(x > 4); // FULL: `x > 4` since `x = 5`
-    }
-}
diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected
deleted file mode 100644
index fedfec8b2a1e..000000000000
--- a/tests/coverage/reachable/bounds/reachable_fail/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL
-coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE
-coverage/reachable/bounds/reachable_fail/test.rs, 10, PARTIAL
-coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/bounds/reachable_fail/test.rs b/tests/coverage/reachable/bounds/reachable_fail/test.rs
deleted file mode 100644
index cebd78b2d5d9..000000000000
--- a/tests/coverage/reachable/bounds/reachable_fail/test.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-fn get(s: &[i16], index: usize) -> i16 {
-    s[index] // PARTIAL: `s[index]` is covered, but `index = 15` induces a failure
-} // NONE: `index = 15` caused failure earlier
-
-#[kani::proof]
-fn main() {
-    get(&[7, -83, 19], 15);
-} // NONE: `index = 15` caused failure earlier
diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected
deleted file mode 100644
index c1ac77404680..000000000000
--- a/tests/coverage/reachable/div-zero/reachable_fail/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL
-coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE
-coverage/reachable/div-zero/reachable_fail/test.rs, 10, PARTIAL
-coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/div-zero/reachable_fail/test.rs b/tests/coverage/reachable/div-zero/reachable_fail/test.rs
deleted file mode 100644
index 5f69005ee712..000000000000
--- a/tests/coverage/reachable/div-zero/reachable_fail/test.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-fn div(x: u16, y: u16) -> u16 {
-    x / y // PARTIAL: `y = 0` causes failure, but `x / y` is `COVERED`
-}
-
-#[kani::proof]
-fn main() {
-    div(678, 0);
-}
diff --git a/tests/coverage/reachable/div-zero/reachable_pass/expected b/tests/coverage/reachable/div-zero/reachable_pass/expected
deleted file mode 100644
index c7bfb5961c0b..000000000000
--- a/tests/coverage/reachable/div-zero/reachable_pass/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/reachable/div-zero/reachable_pass/test.rs, 5, PARTIAL
-coverage/reachable/div-zero/reachable_pass/test.rs, 6, FULL
-coverage/reachable/div-zero/reachable_pass/test.rs, 10, FULL
-coverage/reachable/div-zero/reachable_pass/test.rs, 11, FULL
diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected
deleted file mode 100644
index d45edcc37a63..000000000000
--- a/tests/coverage/reachable/overflow/reachable_fail/expected
+++ /dev/null
@@ -1,5 +0,0 @@
-coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL
-coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL
-coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL
-coverage/reachable/overflow/reachable_fail/test.rs, 14, PARTIAL
-coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE
diff --git a/tests/coverage/reachable/overflow/reachable_pass/expected b/tests/coverage/reachable/overflow/reachable_pass/expected
deleted file mode 100644
index 5becf2cd23e7..000000000000
--- a/tests/coverage/reachable/overflow/reachable_pass/expected
+++ /dev/null
@@ -1,7 +0,0 @@
-coverage/reachable/overflow/reachable_pass/test.rs, 8, FULL
-coverage/reachable/overflow/reachable_pass/test.rs, 9, FULL
-coverage/reachable/overflow/reachable_pass/test.rs, 13, FULL
-coverage/reachable/overflow/reachable_pass/test.rs, 14, FULL
-coverage/reachable/overflow/reachable_pass/test.rs, 15, FULL
-coverage/reachable/overflow/reachable_pass/test.rs, 16, FULL
-coverage/reachable/overflow/reachable_pass/test.rs, 17, FULL
diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected
deleted file mode 100644
index 7852461e4f57..000000000000
--- a/tests/coverage/reachable/rem-zero/reachable_fail/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL
-coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE
-coverage/reachable/rem-zero/reachable_fail/test.rs, 10, PARTIAL
-coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE
diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/test.rs b/tests/coverage/reachable/rem-zero/reachable_fail/test.rs
deleted file mode 100644
index 400c7e02340b..000000000000
--- a/tests/coverage/reachable/rem-zero/reachable_fail/test.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-fn rem(x: u16, y: u16) -> u16 {
-    x % y // PARTIAL: `x % y` is covered but induces a division failure
-} // NONE: Caused by division failure earlier
-
-#[kani::proof]
-fn main() {
-    rem(678, 0);
-} // NONE: Caused by division failure earlier
diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/expected b/tests/coverage/reachable/rem-zero/reachable_pass/expected
deleted file mode 100644
index f3d5934d785d..000000000000
--- a/tests/coverage/reachable/rem-zero/reachable_pass/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/reachable/rem-zero/reachable_pass/test.rs, 5, PARTIAL
-coverage/reachable/rem-zero/reachable_pass/test.rs, 6, FULL
-coverage/reachable/rem-zero/reachable_pass/test.rs, 10, FULL
-coverage/reachable/rem-zero/reachable_pass/test.rs, 11, FULL
diff --git a/tests/coverage/reachable/rem-zero/reachable_pass/test.rs b/tests/coverage/reachable/rem-zero/reachable_pass/test.rs
deleted file mode 100644
index 41ed28f7b903..000000000000
--- a/tests/coverage/reachable/rem-zero/reachable_pass/test.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-fn rem(x: u16, y: u16) -> u16 {
-    if y != 0 { x % y } else { 0 }
-}
-
-#[kani::proof]
-fn main() {
-    rem(11, 3);
-}
diff --git a/tests/coverage/unreachable/abort/expected b/tests/coverage/unreachable/abort/expected
deleted file mode 100644
index 473b0f5a8d4d..000000000000
--- a/tests/coverage/unreachable/abort/expected
+++ /dev/null
@@ -1,7 +0,0 @@
-coverage/unreachable/abort/main.rs, 10, PARTIAL
-coverage/unreachable/abort/main.rs, 11, FULL
-coverage/unreachable/abort/main.rs, 13, FULL
-coverage/unreachable/abort/main.rs, 15, FULL
-coverage/unreachable/abort/main.rs, 17, NONE
-coverage/unreachable/abort/main.rs, 20, NONE
-coverage/unreachable/abort/main.rs, 21, NONE
diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected
deleted file mode 100644
index 9bc6d8faa4f9..000000000000
--- a/tests/coverage/unreachable/assert/expected
+++ /dev/null
@@ -1,7 +0,0 @@
-coverage/unreachable/assert/test.rs, 6, FULL
-coverage/unreachable/assert/test.rs, 7, PARTIAL
-coverage/unreachable/assert/test.rs, 9, PARTIAL
-coverage/unreachable/assert/test.rs, 10, NONE
-coverage/unreachable/assert/test.rs, 12, NONE
-coverage/unreachable/assert/test.rs, 16, FULL
-coverage/unreachable/assert/test.rs, 18, FULL
diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected
deleted file mode 100644
index 9b13c3c96ded..000000000000
--- a/tests/coverage/unreachable/assert_eq/expected
+++ /dev/null
@@ -1,5 +0,0 @@
-coverage/unreachable/assert_eq/test.rs, 6, FULL
-coverage/unreachable/assert_eq/test.rs, 7, FULL
-coverage/unreachable/assert_eq/test.rs, 8, PARTIAL
-coverage/unreachable/assert_eq/test.rs, 9, NONE
-coverage/unreachable/assert_eq/test.rs, 11, FULL
diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected
deleted file mode 100644
index f027f432e280..000000000000
--- a/tests/coverage/unreachable/assert_ne/expected
+++ /dev/null
@@ -1,6 +0,0 @@
-coverage/unreachable/assert_ne/test.rs, 6, FULL
-coverage/unreachable/assert_ne/test.rs, 7, FULL
-coverage/unreachable/assert_ne/test.rs, 8, FULL
-coverage/unreachable/assert_ne/test.rs, 10, PARTIAL
-coverage/unreachable/assert_ne/test.rs, 11, NONE
-coverage/unreachable/assert_ne/test.rs, 14, FULL
diff --git a/tests/coverage/unreachable/assume_assert/expected b/tests/coverage/unreachable/assume_assert/expected
deleted file mode 100644
index 8c1ae8a247d2..000000000000
--- a/tests/coverage/unreachable/assume_assert/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/unreachable/assume_assert/main.rs, 5, FULL
-coverage/unreachable/assume_assert/main.rs, 6, FULL
-coverage/unreachable/assume_assert/main.rs, 7, NONE
-coverage/unreachable/assume_assert/main.rs, 8, NONE
diff --git a/tests/coverage/unreachable/assume_assert/main.rs b/tests/coverage/unreachable/assume_assert/main.rs
deleted file mode 100644
index c4d5d65c6640..000000000000
--- a/tests/coverage/unreachable/assume_assert/main.rs
+++ /dev/null
@@ -1,8 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-#[kani::proof]
-fn check_assume_assert() {
-    let a: u8 = kani::any();
-    kani::assume(false);
-    assert!(a < 5);
-}
diff --git a/tests/coverage/unreachable/bounds/expected b/tests/coverage/unreachable/bounds/expected
deleted file mode 100644
index 610372000a01..000000000000
--- a/tests/coverage/unreachable/bounds/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/unreachable/bounds/test.rs, 5, PARTIAL
-coverage/unreachable/bounds/test.rs, 6, FULL
-coverage/unreachable/bounds/test.rs, 11, FULL
-coverage/unreachable/bounds/test.rs, 12, FULL
diff --git a/tests/coverage/unreachable/bounds/test.rs b/tests/coverage/unreachable/bounds/test.rs
deleted file mode 100644
index c37c9d0dcad6..000000000000
--- a/tests/coverage/unreachable/bounds/test.rs
+++ /dev/null
@@ -1,12 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-fn get(s: &[i16], index: usize) -> i16 {
-    if index < s.len() { s[index] } else { -1 }
-}
-
-#[kani::proof]
-fn main() {
-    //get(&[7, -83, 19], 2);
-    get(&[5, 206, -46, 321, 8], 8);
-}
diff --git a/tests/coverage/unreachable/break/expected b/tests/coverage/unreachable/break/expected
deleted file mode 100644
index dcb013c50c3d..000000000000
--- a/tests/coverage/unreachable/break/expected
+++ /dev/null
@@ -1,9 +0,0 @@
-coverage/unreachable/break/main.rs, 5, PARTIAL
-coverage/unreachable/break/main.rs, 6, FULL
-coverage/unreachable/break/main.rs, 7, FULL
-coverage/unreachable/break/main.rs, 11, NONE
-coverage/unreachable/break/main.rs, 12, PARTIAL
-coverage/unreachable/break/main.rs, 16, FULL
-coverage/unreachable/break/main.rs, 17, FULL
-coverage/unreachable/break/main.rs, 18, FULL
-coverage/unreachable/break/main.rs, 19, FULL
diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected
deleted file mode 100644
index a2d296f0f9a3..000000000000
--- a/tests/coverage/unreachable/check_id/expected
+++ /dev/null
@@ -1,16 +0,0 @@
-coverage/unreachable/check_id/main.rs, 5, FULL
-coverage/unreachable/check_id/main.rs, 6, PARTIAL
-coverage/unreachable/check_id/main.rs, 8, NONE
-coverage/unreachable/check_id/main.rs, 10, FULL
-coverage/unreachable/check_id/main.rs, 14, FULL
-coverage/unreachable/check_id/main.rs, 15, FULL
-coverage/unreachable/check_id/main.rs, 16, FULL
-coverage/unreachable/check_id/main.rs, 17, FULL
-coverage/unreachable/check_id/main.rs, 18, FULL
-coverage/unreachable/check_id/main.rs, 19, FULL
-coverage/unreachable/check_id/main.rs, 20, FULL
-coverage/unreachable/check_id/main.rs, 21, FULL
-coverage/unreachable/check_id/main.rs, 22, FULL
-coverage/unreachable/check_id/main.rs, 23, FULL
-coverage/unreachable/check_id/main.rs, 24, PARTIAL
-coverage/unreachable/check_id/main.rs, 25, NONE
diff --git a/tests/coverage/unreachable/check_id/main.rs b/tests/coverage/unreachable/check_id/main.rs
deleted file mode 100644
index 8273a9bcc679..000000000000
--- a/tests/coverage/unreachable/check_id/main.rs
+++ /dev/null
@@ -1,25 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-fn foo(x: i32) {
-    assert!(1 + 1 == 2);
-    if x < 9 {
-        // unreachable
-        assert!(2 + 2 == 4);
-    }
-}
-
-#[kani::proof]
-fn main() {
-    assert!(1 + 1 == 2);
-    let x = if kani::any() { 33 } else { 57 };
-    foo(x);
-    assert!(1 + 1 == 2);
-    assert!(1 + 1 == 2);
-    assert!(1 + 1 == 2);
-    assert!(1 + 1 == 2);
-    assert!(1 + 1 == 2);
-    assert!(1 + 1 == 2);
-    assert!(1 + 1 == 2);
-    assert!(3 + 3 == 5);
-}
diff --git a/tests/coverage/unreachable/compare/expected b/tests/coverage/unreachable/compare/expected
deleted file mode 100644
index 6187e232cbe7..000000000000
--- a/tests/coverage/unreachable/compare/expected
+++ /dev/null
@@ -1,7 +0,0 @@
-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, 14, FULL
-coverage/unreachable/compare/main.rs, 16, FULL
diff --git a/tests/coverage/unreachable/contradiction/expected b/tests/coverage/unreachable/contradiction/expected
deleted file mode 100644
index 4234fc328e1e..000000000000
--- a/tests/coverage/unreachable/contradiction/expected
+++ /dev/null
@@ -1,7 +0,0 @@
-coverage/unreachable/contradiction/main.rs, 5, FULL
-coverage/unreachable/contradiction/main.rs, 6, FULL
-coverage/unreachable/contradiction/main.rs, 7, FULL
-coverage/unreachable/contradiction/main.rs, 8, PARTIAL
-coverage/unreachable/contradiction/main.rs, 9, NONE
-coverage/unreachable/contradiction/main.rs, 12, FULL
-coverage/unreachable/contradiction/main.rs, 14, FULL
diff --git a/tests/coverage/unreachable/debug-assert/expected b/tests/coverage/unreachable/debug-assert/expected
deleted file mode 100644
index 25fdfed4c863..000000000000
--- a/tests/coverage/unreachable/debug-assert/expected
+++ /dev/null
@@ -1,4 +0,0 @@
-coverage/unreachable/debug-assert/main.rs, 6, PARTIAL
-coverage/unreachable/debug-assert/main.rs, 7, PARTIAL
-coverage/unreachable/debug-assert/main.rs, 8, NONE
-coverage/unreachable/debug-assert/main.rs, 10, NONE
diff --git a/tests/coverage/unreachable/debug-assert/main.rs b/tests/coverage/unreachable/debug-assert/main.rs
deleted file mode 100644
index ab3ab41e47d0..000000000000
--- a/tests/coverage/unreachable/debug-assert/main.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-#[kani::proof]
-fn main() {
-    for i in 0..4 {
-        debug_assert!(i > 0, "This should fail and stop the execution");
-        assert!(i == 0, "This should be unreachable");
-    }
-}
diff --git a/tests/coverage/unreachable/divide/expected b/tests/coverage/unreachable/divide/expected
deleted file mode 100644
index 63081358941a..000000000000
--- a/tests/coverage/unreachable/divide/expected
+++ /dev/null
@@ -1,7 +0,0 @@
-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
-coverage/unreachable/divide/main.rs, 16, FULL
-coverage/unreachable/divide/main.rs, 17, FULL
diff --git a/tests/coverage/unreachable/divide/main.rs b/tests/coverage/unreachable/divide/main.rs
deleted file mode 100644
index ba6afab83135..000000000000
--- a/tests/coverage/unreachable/divide/main.rs
+++ /dev/null
@@ -1,19 +0,0 @@
-// 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 {
-        panic!("Division by zero");
-    }
-}
-
-#[kani::proof]
-fn main() {
-    let y: i32 = kani::any();
-    kani::assume(y != 0);
-    let result = divide(10, y);
-    assert_eq!(result, 5);
-}
diff --git a/tests/coverage/unreachable/early-return/expected b/tests/coverage/unreachable/early-return/expected
deleted file mode 100644
index 466c1775408b..000000000000
--- a/tests/coverage/unreachable/early-return/expected
+++ /dev/null
@@ -1,10 +0,0 @@
-coverage/unreachable/early-return/main.rs, 5, PARTIAL
-coverage/unreachable/early-return/main.rs, 6, FULL
-coverage/unreachable/early-return/main.rs, 7, FULL
-coverage/unreachable/early-return/main.rs, 10, NONE
-coverage/unreachable/early-return/main.rs, 11, PARTIAL
-coverage/unreachable/early-return/main.rs, 15, FULL
-coverage/unreachable/early-return/main.rs, 16, FULL
-coverage/unreachable/early-return/main.rs, 17, FULL
-coverage/unreachable/early-return/main.rs, 18, FULL
-coverage/unreachable/early-return/main.rs, 19, FULL
diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected
deleted file mode 100644
index 8b481863a163..000000000000
--- a/tests/coverage/unreachable/if-statement/expected
+++ /dev/null
@@ -1,10 +0,0 @@
-coverage/unreachable/if-statement/main.rs, 5, PARTIAL
-coverage/unreachable/if-statement/main.rs, 7, PARTIAL
-coverage/unreachable/if-statement/main.rs, 8, NONE
-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
diff --git a/tests/coverage/unreachable/multiple-harnesses/expected b/tests/coverage/unreachable/multiple-harnesses/expected
deleted file mode 100644
index 17a52666c08d..000000000000
--- a/tests/coverage/unreachable/multiple-harnesses/expected
+++ /dev/null
@@ -1,39 +0,0 @@
-Checking harness fully_covered...
-coverage/unreachable/multiple-harnesses/main.rs, 5, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 7, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 8, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 9, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 11, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 13, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 14, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 15, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 17, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 20, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 21, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 23, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 26, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 40, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 41, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 42, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 43, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 44, FULL
-
-Checking harness mostly_covered...
-coverage/unreachable/multiple-harnesses/main.rs, 5, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 7, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 8, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 9, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 11, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 13, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 14, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 15, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 17, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 20, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 21, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 23, NONE
-coverage/unreachable/multiple-harnesses/main.rs, 26, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 31, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 32, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 33, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 34, FULL
-coverage/unreachable/multiple-harnesses/main.rs, 35, FULL
diff --git a/tests/coverage/unreachable/return/expected b/tests/coverage/unreachable/return/expected
deleted file mode 100644
index 139f81840aab..000000000000
--- a/tests/coverage/unreachable/return/expected
+++ /dev/null
@@ -1,8 +0,0 @@
-coverage/unreachable/return/main.rs, 5, FULL
-coverage/unreachable/return/main.rs, 6, FULL
-coverage/unreachable/return/main.rs, 9, NONE
-coverage/unreachable/return/main.rs, 10, PARTIAL
-coverage/unreachable/return/main.rs, 14, FULL
-coverage/unreachable/return/main.rs, 15, FULL
-coverage/unreachable/return/main.rs, 16, FULL
-coverage/unreachable/return/main.rs, 17, FULL
diff --git a/tests/coverage/unreachable/return/main.rs b/tests/coverage/unreachable/return/main.rs
deleted file mode 100644
index ccd76a5b4f8e..000000000000
--- a/tests/coverage/unreachable/return/main.rs
+++ /dev/null
@@ -1,17 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-fn greet(is_guest: bool) -> &'static str {
-    if is_guest {
-        return "Welcome, Guest!";
-    }
-    // This part is unreachable if is_guest is true.
-    "Hello, User!"
-}
-
-#[kani::proof]
-fn main() {
-    let is_guest = true;
-    let message = greet(is_guest);
-    assert_eq!(message, "Welcome, Guest!");
-}
diff --git a/tests/coverage/unreachable/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected
deleted file mode 100644
index 624aa520edc9..000000000000
--- a/tests/coverage/unreachable/tutorial_unreachable/expected
+++ /dev/null
@@ -1,5 +0,0 @@
-coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL
-coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL
-coverage/unreachable/tutorial_unreachable/main.rs, 8, PARTIAL
-coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE
-coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL
diff --git a/tests/coverage/unreachable/tutorial_unreachable/main.rs b/tests/coverage/unreachable/tutorial_unreachable/main.rs
deleted file mode 100644
index c56e591446cf..000000000000
--- a/tests/coverage/unreachable/tutorial_unreachable/main.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-#[kani::proof]
-fn unreachable_example() {
-    let x = 5;
-    let y = x + 2;
-    if x > y {
-        assert!(x < 8);
-    }
-}
diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected
deleted file mode 100644
index 8fa3ec8b870f..000000000000
--- a/tests/coverage/unreachable/variant/expected
+++ /dev/null
@@ -1,10 +0,0 @@
-coverage/unreachable/variant/main.rs, 15, FULL
-coverage/unreachable/variant/main.rs, 16, NONE
-coverage/unreachable/variant/main.rs, 17, NONE
-coverage/unreachable/variant/main.rs, 18, FULL
-coverage/unreachable/variant/main.rs, 19, NONE
-coverage/unreachable/variant/main.rs, 21, NONE
-coverage/unreachable/variant/main.rs, 23, FULL
-coverage/unreachable/variant/main.rs, 27, FULL
-coverage/unreachable/variant/main.rs, 28, FULL
-coverage/unreachable/variant/main.rs, 29, FULL
diff --git a/tests/coverage/unreachable/vectors/expected b/tests/coverage/unreachable/vectors/expected
deleted file mode 100644
index e47941f17db2..000000000000
--- a/tests/coverage/unreachable/vectors/expected
+++ /dev/null
@@ -1,6 +0,0 @@
-coverage/unreachable/vectors/main.rs, 8, FULL
-coverage/unreachable/vectors/main.rs, 11, FULL
-coverage/unreachable/vectors/main.rs, 13, PARTIAL
-coverage/unreachable/vectors/main.rs, 15, NONE
-coverage/unreachable/vectors/main.rs, 17, FULL
-coverage/unreachable/vectors/main.rs, 19, FULL
diff --git a/tests/coverage/unreachable/vectors/main.rs b/tests/coverage/unreachable/vectors/main.rs
deleted file mode 100644
index a44c4bb47c3d..000000000000
--- a/tests/coverage/unreachable/vectors/main.rs
+++ /dev/null
@@ -1,19 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-//! Checks coverage results in an example with a guarded out-of-bounds access.
-
-#[kani::proof]
-fn main() {
-    let numbers = vec![1, 2, 3, 4, 5];
-
-    // Attempt to access the 10th element of the vector, which is out of bounds.
-    let tenth_element = numbers.get(9);
-
-    if let Some(value) = tenth_element {
-        // This part is unreachable since the vector has only 5 elements (indices 0 to 4).
-        println!("The 10th element is: {}", value);
-    } else {
-        println!("The 10th element is out of bounds!");
-    }
-}
diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected
deleted file mode 100644
index dc66d3e823d3..000000000000
--- a/tests/coverage/unreachable/while-loop-break/expected
+++ /dev/null
@@ -1,11 +0,0 @@
-coverage/unreachable/while-loop-break/main.rs, 8, FULL
-coverage/unreachable/while-loop-break/main.rs, 9, PARTIAL
-coverage/unreachable/while-loop-break/main.rs, 10, FULL
-coverage/unreachable/while-loop-break/main.rs, 11, FULL
-coverage/unreachable/while-loop-break/main.rs, 13, FULL
-coverage/unreachable/while-loop-break/main.rs, 15, NONE
-coverage/unreachable/while-loop-break/main.rs, 16, PARTIAL
-coverage/unreachable/while-loop-break/main.rs, 20, FULL
-coverage/unreachable/while-loop-break/main.rs, 21, FULL
-coverage/unreachable/while-loop-break/main.rs, 22, FULL
-coverage/unreachable/while-loop-break/main.rs, 23, FULL
diff --git a/tests/coverage/while-loop-break/expected b/tests/coverage/while-loop-break/expected
new file mode 100644
index 000000000000..34afef9ee12c
--- /dev/null
+++ b/tests/coverage/while-loop-break/expected
@@ -0,0 +1,13 @@
+Source-based code coverage results:
+
+main.rs (find_first_negative)\
+ * 7:1 - 8:22 COVERED\
+ * 9:11 - 9:29 COVERED\
+ * 10:12 - 10:27 COVERED\
+ * 11:20 - 11:37 COVERED\
+ * 12:10 - 13:19 COVERED\
+ * 15:5 - 15:9 UNCOVERED\
+ * 16:1 - 16:2 COVERED
+
+main.rs (main)\
+ * 19:1 - 23:2 COVERED
diff --git a/tests/coverage/unreachable/while-loop-break/main.rs b/tests/coverage/while-loop-break/main.rs
similarity index 100%
rename from tests/coverage/unreachable/while-loop-break/main.rs
rename to tests/coverage/while-loop-break/main.rs
diff --git a/tests/ui/save-coverage-results/expected b/tests/ui/save-coverage-results/expected
new file mode 100644
index 000000000000..77c9a0c33dcb
--- /dev/null
+++ b/tests/ui/save-coverage-results/expected
@@ -0,0 +1,3 @@
+Source-based code coverage results:
+
+[info] Coverage results saved to 
diff --git a/tests/ui/save-coverage-results/test.rs b/tests/ui/save-coverage-results/test.rs
new file mode 100644
index 000000000000..0a422280e51d
--- /dev/null
+++ b/tests/ui/save-coverage-results/test.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --coverage -Zsource-coverage
+
+//! Checks that we print a line which points the user to the path where coverage
+//! results have been saved. The line should look like:
+//! ```
+//! [info] Coverage results saved to /path/to/outdir/kanicov_YYYY-MM-DD_hh-mm
+//! ```
+
+fn _other_function() {
+    println!("Hello, world!");
+}
+
+fn test_cov(val: u32) -> bool {
+    if val < 3 || val == 42 { true } else { false }
+}
+
+#[cfg_attr(kani, kani::proof)]
+fn main() {
+    let test1 = test_cov(1);
+    let test2 = test_cov(2);
+    assert!(test1);
+    assert!(test2);
+}
diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index 50f1e3035ac8..c8387c691296 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -320,7 +320,7 @@ impl<'test> TestCx<'test> {
             kani.env("RUSTFLAGS", self.props.compile_flags.join(" "));
         }
         kani.arg(&self.testpaths.file).args(&self.props.kani_flags);
-        kani.arg("--coverage").args(["-Z", "line-coverage"]);
+        kani.arg("--coverage").args(["-Z", "source-coverage"]);
 
         if !self.props.cbmc_flags.is_empty() {
             kani.arg("--cbmc-args").args(&self.props.cbmc_flags);