diff --git a/Cargo.lock b/Cargo.lock
index 580cdf70946a..c4709fbe446e 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -769,6 +769,20 @@ dependencies = [
  "tracing-tree 0.4.0",
 ]
 
+[[package]]
+name = "kani-cov"
+version = "0.1.0"
+dependencies = [
+ "anyhow",
+ "clap",
+ "console",
+ "serde",
+ "serde_derive",
+ "serde_json",
+ "tree-sitter",
+ "tree-sitter-rust",
+]
+
 [[package]]
 name = "kani-driver"
 version = "0.56.0"
@@ -1811,6 +1825,34 @@ dependencies = [
  "tracing-subscriber",
 ]
 
+[[package]]
+name = "tree-sitter"
+version = "0.23.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "20f4cd3642c47a85052a887d86704f4eac272969f61b686bdd3f772122aabaff"
+dependencies = [
+ "cc",
+ "regex",
+ "regex-syntax 0.8.5",
+ "tree-sitter-language",
+]
+
+[[package]]
+name = "tree-sitter-language"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2545046bd1473dac6c626659cc2567c6c0ff302fc8b84a56c4243378276f7f57"
+
+[[package]]
+name = "tree-sitter-rust"
+version = "0.21.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "277690f420bf90741dea984f3da038ace46c4fe6047cba57a66822226cde1c93"
+dependencies = [
+ "cc",
+ "tree-sitter",
+]
+
 [[package]]
 name = "typed-arena"
 version = "2.0.2"
diff --git a/Cargo.toml b/Cargo.toml
index 42c6f2c722b6..3c61638025e5 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -40,6 +40,7 @@ members = [
   "library/std",
   "tools/compiletest",
   "tools/build-kani",
+  "tools/kani-cov",
   "tools/scanner",
   "kani-driver",
   "kani-compiler",
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index be2548235ce6..728129d784b6 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -70,6 +70,9 @@ echo "--- Compiletest configuration"
 cargo run -p compiletest --quiet -- --suite kani --mode cargo-kani --dry-run --verbose
 echo "-----------------------------"
 
+# Build `kani-cov`
+cargo build -p kani-cov
+
 # Extract testing suite information and run compiletest
 for testp in "${TESTS[@]}"; do
   testl=($testp)
diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected
index 91142ebf94fc..e9c9727a6f03 100644
--- a/tests/coverage/abort/expected
+++ b/tests/coverage/abort/expected
@@ -1,13 +1,21 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Test that the abort() function is respected and nothing beyond it will execute.\
+   5|     | \
+   6|     | use std::process;\
+   7|     | \
+   8|     | #[kani::proof]\
+   9|    1| fn main() {\
+  10|    1|     for i in 0..4 {\
+  11|     |         if i == 1 {\
+  12|     |             // This comes first and it should be reachable.\
+  13|    1|             process::abort();\
+  14|    1|         }\
+  15|    1|         if i == 2 {\
+  16|     |             // This should never happen.\
+  17|    0|             ```process::exit(1)''';\
+  18|    1|         } \
+  19|     |     }\
+  20|    0|     ```assert!'''(false, ```"This is unreachable"''');\
+  21|     | }\
diff --git a/tests/coverage/assert/expected b/tests/coverage/assert/expected
index 46bb664cf6f5..c2f3ffbe733e 100644
--- a/tests/coverage/assert/expected
+++ b/tests/coverage/assert/expected
@@ -1,9 +1,18 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | #[kani::proof]\
+   5|    1| fn foo() {\
+   6|    1|     let x: i32 = kani::any();\
+   7|    1|     if x > 5 {\
+   8|     |         // fails\
+   9|    1|         assert!(x < 4);\
+  10|    1|         if x < 3 ```{'''\
+  11|    0| ```            // unreachable'''\
+  12|    0| ```            assert!(x == 2);'''\
+  13|    0| ```        }'''``` '''\
+  14|    1|     } else {\
+  15|    1|         // passes\
+  16|    1|         assert!(x <= 5);\
+  17|    1|     }\
+  18|     | }\
diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected
index c2eee7adf803..0cc1e01fbca9 100644
--- a/tests/coverage/assert_eq/expected
+++ b/tests/coverage/assert_eq/expected
@@ -1,8 +1,11 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | #[kani::proof]\
+   5|    1| fn main() {\
+   6|    1|     let x: i32 = kani::any();\
+   7|    1|     let y = if x > 10 { 15 } else { 33 };\
+   8|    0|     if y > 50 ```{'''\
+   9|    0| ```        assert_eq!(y, 55);'''\
+  10|    1| ```    }'''\
+  11|     | }\
diff --git a/tests/coverage/assert_ne/expected b/tests/coverage/assert_ne/expected
index c9b727da0f82..73055a14af10 100644
--- a/tests/coverage/assert_ne/expected
+++ b/tests/coverage/assert_ne/expected
@@ -1,9 +1,14 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | #[kani::proof]\
+   5|    1| fn main() {\
+   6|    1|     let x: u32 = kani::any();\
+   7|    1|     if x > 0 {\
+   8|    1|         let y = x / 2;\
+   9|    1|         // y is strictly less than x\
+  10|    1|         if y == x ```{'''\
+  11|    0| ```            assert_ne!(y, 1);'''\
+  12|    1| ```        }'''\
+  13|    1|     }\
+  14|     | }\
diff --git a/tests/coverage/break/expected b/tests/coverage/break/expected
index 739735cdf1a2..e1570030f6ae 100644
--- a/tests/coverage/break/expected
+++ b/tests/coverage/break/expected
@@ -1,13 +1,19 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    1| fn find_positive(nums: &[i32]) -> Option<i32> {\
+   5|    1|     for &num in nums {\
+   6|     |         if num > 0 {\
+   7|    1|             return Some(num);\
+   8|    1|         } \
+   9|     |     }\
+  10|     |     // `None` is unreachable because there is at least one positive number.\
+  11|    0|     ```None'''\
+  12|     | }\
+  13|     | \
+  14|     | #[kani::proof]\
+  15|    1| fn main() {\
+  16|    1|     let numbers = [-3, -1, 0, 2, 4];\
+  17|    1|     let result = find_positive(&numbers);\
+  18|    1|     assert_eq!(result, Some(2));\
+  19|     | }\
diff --git a/tests/coverage/compare/expected b/tests/coverage/compare/expected
index 153dbfa37d80..3a59376e8ce3 100644
--- a/tests/coverage/compare/expected
+++ b/tests/coverage/compare/expected
@@ -1,11 +1,16 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    1| fn compare(x: u16, y: u16) -> u16 {\
+   5|    1|     // The case where `x < y` isn't possible so its region is `UNCOVERED`\
+   6|    1|     if x >= y { 1 } else { ```0''' }\
+   7|     | }\
+   8|     | \
+   9|     | #[kani::proof]\
+  10|    1| fn main() {\
+  11|    1|     let x: u16 = kani::any();\
+  12|    1|     let y: u16 = kani::any();\
+  13|    1|     if x >= y {\
+  14|    1|         compare(x, y);\
+  15|    1|     } \
+  16|     | }\
diff --git a/tests/coverage/contradiction/expected b/tests/coverage/contradiction/expected
index db3676d7da15..7befb09a1f9e 100644
--- a/tests/coverage/contradiction/expected
+++ b/tests/coverage/contradiction/expected
@@ -1,9 +1,14 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | #[kani::proof]\
+   4|    1| fn contradiction() {\
+   5|    1|     let x: u8 = kani::any();\
+   6|    1|     let mut y: u8 = 0;\
+   7|    1|     if x > 5 {\
+   8|    1|         if x < 2 ```{'''\
+   9|    0| ```            y = x;'''\
+  10|    1| ```        }'''\
+  11|    1|     } else {\
+  12|    1|         assert!(x < 10);\
+  13|    1|     }\
+  14|     | }\
diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected
index fbe57690d347..82ad7c992ca3 100644
--- a/tests/coverage/debug-assert/expected
+++ b/tests/coverage/debug-assert/expected
@@ -1,10 +1,15 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! This test checks that the regions after the `debug_assert` macro are\
+   5|     | //! `UNCOVERED`. In fact, for this example, the region associated to `"This\
+   6|     | //! should fail and stop the execution"` is also `UNCOVERED` because the macro\
+   7|     | //! calls span two regions each.\
+   8|     | \
+   9|     | #[kani::proof]\
+  10|    1| fn main() {\
+  11|    1|     for i in 0..4 {\
+  12|    0|         debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
+  13|    0|         ```assert!(i == 0''', ```"This should be unreachable"''');\
+  14|     |     }\
+  15|     | }\
diff --git a/tests/coverage/div-zero/expected b/tests/coverage/div-zero/expected
index f351005f4f22..503fa9a22a05 100644
--- a/tests/coverage/div-zero/expected
+++ b/tests/coverage/div-zero/expected
@@ -1,9 +1,11 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    1| fn div(x: u16, y: u16) -> u16 {\
+   5|    1|     if y != 0 { x / y } else { ```0''' }\
+   6|     | }\
+   7|     | \
+   8|     | #[kani::proof]\
+   9|    1| fn main() {\
+  10|    1|     div(11, 3);\
+  11|     | }\
diff --git a/tests/coverage/early-return/expected b/tests/coverage/early-return/expected
index 53cde3abeaf8..efdd71ee91f0 100644
--- a/tests/coverage/early-return/expected
+++ b/tests/coverage/early-return/expected
@@ -1,12 +1,19 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    1| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
+   5|    1|     for (index, &num) in nums.iter().enumerate() {\
+   6|     |         if num == target {\
+   7|    1|             return Some(index);\
+   8|    1|         } \
+   9|     |     }\
+  10|    0|     ```None'''\
+  11|     | }\
+  12|     | \
+  13|     | #[kani::proof]\
+  14|    1| fn main() {\
+  15|    1|     let numbers = [10, 20, 30, 40, 50];\
+  16|    1|     let target = 30;\
+  17|    1|     let result = find_index(&numbers, target);\
+  18|    1|     assert_eq!(result, Some(2));\
+  19|     | }\
diff --git a/tests/coverage/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected
index 4e8382d10a6f..87b3b80f556d 100644
--- a/tests/coverage/if-statement-multi/expected
+++ b/tests/coverage/if-statement-multi/expected
@@ -1,11 +1,26 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | // kani-flags: --coverage -Zsource-coverage\
+   4|     | \
+   5|     | //! Checks that we are covering all regions except\
+   6|     | //!  * the `val == 42` condition\
+   7|     | //!  * the `false` branch\
+   8|     | //!\
+   9|     | //! No coverage information is shown for `_other_function` because it's sliced\
+  10|     | //! off: <https://github.com/model-checking/kani/issues/3445>\
+  11|     | \
+  12|    0| ```fn _other_function() {'''\
+  13|    0| ```    println!("Hello, world!");'''\
+  14|    0| ```}'''\
+  15|     | \
+  16|    1| fn test_cov(val: u32) -> bool {\
+  17|    1|     if val < 3 || ```val == 42''' { true } else { ```false''' }\
+  18|     | }\
+  19|     | \
+  20|     | #[cfg_attr(kani, kani::proof)]\
+  21|    1| fn main() {\
+  22|    1|     let test1 = test_cov(1);\
+  23|    1|     let test2 = test_cov(2);\
+  24|    1|     assert!(test1);\
+  25|    1|     assert!(test2);\
+  26|     | }\
diff --git a/tests/coverage/if-statement/expected b/tests/coverage/if-statement/expected
index b85b95de9c84..85efc027aa04 100644
--- a/tests/coverage/if-statement/expected
+++ b/tests/coverage/if-statement/expected
@@ -1,14 +1,20 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    1| fn check_number(num: i32) -> &'static str {\
+   5|    1|     if num > 0 {\
+   6|     |         // The next line is partially covered\
+   7|    1|         if num % 2 == 0 { ```"Positive and Even"''' } else { "Positive and Odd" }\
+   8|    0|     } else if ```num < 0''' {\
+   9|    0|         ```"Negative"'''\
+  10|     |     } else {\
+  11|    0|         ```"Zero"'''\
+  12|     |     }\
+  13|     | }\
+  14|     | \
+  15|     | #[kani::proof]\
+  16|    1| fn main() {\
+  17|    1|     let number = 7;\
+  18|    1|     let result = check_number(number);\
+  19|    1|     assert_eq!(result, "Positive and Odd");\
+  20|     | }\
diff --git a/tests/coverage/known_issues/assert_uncovered_end/expected b/tests/coverage/known_issues/assert_uncovered_end/expected
index ceba065ce424..2f6fca5e4aae 100644
--- a/tests/coverage/known_issues/assert_uncovered_end/expected
+++ b/tests/coverage/known_issues/assert_uncovered_end/expected
@@ -1,9 +1,14 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks that `check_assert` is fully covered. At present, the coverage for\
+   5|     | //! this test reports an uncovered single-column region at the end of the `if`\
+   6|     | //! statement: <https://github.com/model-checking/kani/issues/3455>\
+   7|     | \
+   8|     | #[kani::proof]\
+   9|    1| fn check_assert() {\
+  10|    1|     let x: u32 = kani::any_where(|val| *val == 5);\
+  11|    1|     if x > 3 {\
+  12|    1|         assert!(x > 4);\
+  13|    1|     }``` '''\
+  14|     | }\
diff --git a/tests/coverage/known_issues/assume_assert/expected b/tests/coverage/known_issues/assume_assert/expected
index 55f3235d7d24..a65a36099d05 100644
--- a/tests/coverage/known_issues/assume_assert/expected
+++ b/tests/coverage/known_issues/assume_assert/expected
@@ -1,4 +1,15 @@
-Source-based code coverage results:
-
-main.rs (check_assume_assert)\
- * 11:1 - 15:2 COVERED
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! This test should check that the region after `kani::assume(false)` is\
+   5|     | //! `UNCOVERED`. However, due to a technical limitation in `rustc`'s coverage\
+   6|     | //! instrumentation, only one `COVERED` region is reported for the whole\
+   7|     | //! function. More details in\
+   8|     | //! <https://github.com/model-checking/kani/issues/3441>.\
+   9|     | \
+  10|     | #[kani::proof]\
+  11|    1| fn check_assume_assert() {\
+  12|    1|     let a: u8 = kani::any();\
+  13|    1|     kani::assume(false);\
+  14|    1|     assert!(a < 5);\
+  15|     | }\
diff --git a/tests/coverage/known_issues/out-of-bounds/expected b/tests/coverage/known_issues/out-of-bounds/expected
index 8ab9e2e15627..3924d21de456 100644
--- a/tests/coverage/known_issues/out-of-bounds/expected
+++ b/tests/coverage/known_issues/out-of-bounds/expected
@@ -1,7 +1,15 @@
-Source-based code coverage results:
-
-test.rs (get)\
- * 8:1 - 10:2 COVERED
-
-test.rs (main)\
- * 13:1 - 15:2 COVERED
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! This test should check that the return in `get` is `UNCOVERED`. However, the\
+   5|     | //! coverage results currently report that the whole function is `COVERED`,\
+   6|     | //! likely due to <https://github.com/model-checking/kani/issues/3441>\
+   7|     | \
+   8|    1| fn get(s: &[i16], index: usize) -> i16 {\
+   9|    1|     s[index]\
+  10|     | }\
+  11|     | \
+  12|     | #[kani::proof]\
+  13|    1| fn main() {\
+  14|    1|     get(&[7, -83, 19], 15);\
+  15|     | }\
diff --git a/tests/coverage/known_issues/variant/expected b/tests/coverage/known_issues/variant/expected
index 13383ed3bab0..6445c038f060 100644
--- a/tests/coverage/known_issues/variant/expected
+++ b/tests/coverage/known_issues/variant/expected
@@ -1,14 +1,32 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks coverage results in an example with a `match` statement matching on\
+   5|     | //! all enum variants. Currently, it does not yield the expected results because\
+   6|     | //! it reports the `dir` in the match statement as `UNCOVERED`:\
+   7|     | //! <https://github.com/model-checking/kani/issues/3456>\
+   8|     | \
+   9|     | enum Direction {\
+  10|     |     Up,\
+  11|     |     Down,\
+  12|     |     Left,\
+  13|     |     Right,\
+  14|     | }\
+  15|     | \
+  16|    1| fn print_direction(dir: Direction) {\
+  17|     |     // For some reason, `dir`'s span is reported as `UNCOVERED` too\
+  18|    0|     match ```dir''' {\
+  19|    0|         Direction::Up => ```println!("Going up!")''',\
+  20|    0|         Direction::Down => ```println!("Going down!")''',\
+  21|    1|         Direction::Left => println!("Going left!"),\
+  22|    0|         Direction::Right if 1 == ```1 => println!("Going right!")''',\
+  23|     |         // This part is unreachable since we cover all variants in the match.\
+  24|    0|         _ => ```println!("Not going anywhere!")''',\
+  25|     |     }\
+  26|     | }\
+  27|     | \
+  28|     | #[kani::proof]\
+  29|    1| fn main() {\
+  30|    1|     let direction = Direction::Left;\
+  31|    1|     print_direction(direction);\
+  32|     | }\
diff --git a/tests/coverage/multiple-harnesses/expected b/tests/coverage/multiple-harnesses/expected
index b5362147fed1..6ae834a3bccb 100644
--- a/tests/coverage/multiple-harnesses/expected
+++ b/tests/coverage/multiple-harnesses/expected
@@ -1,37 +1,44 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|    2| fn estimate_size(x: u32) -> u32 {\
+   5|    2|     assert!(x < 4096);\
+   6|    2| \
+   7|    2|     if x < 256 {\
+   8|    2|         if x < 128 {\
+   9|    2|             return 1;\
+  10|     |         } else {\
+  11|    2|             return 3;\
+  12|     |         }\
+  13|    2|     } else if x < 1024 {\
+  14|    2|         if x > 1022 {\
+  15|    2|             return 4;\
+  16|     |         } else {\
+  17|    2|             return 5;\
+  18|     |         }\
+  19|     |     } else {\
+  20|    2|         if x < 2048 {\
+  21|    2|             return 7;\
+  22|     |         } else {\
+  23|    1|             return 9;\
+  24|     |         }\
+  25|     |     }\
+  26|     | }\
+  27|     | \
+  28|     | #[cfg(kani)]\
+  29|     | #[kani::proof]\
+  30|    1| fn mostly_covered() {\
+  31|    1|     let x: u32 = kani::any();\
+  32|    1|     kani::assume(x < 2048);\
+  33|    1|     let y = estimate_size(x);\
+  34|    1|     assert!(y < 10);\
+  35|     | }\
+  36|     | \
+  37|     | #[cfg(kani)]\
+  38|     | #[kani::proof]\
+  39|    1| fn fully_covered() {\
+  40|    1|     let x: u32 = kani::any();\
+  41|    1|     kani::assume(x < 4096);\
+  42|    1|     let y = estimate_size(x);\
+  43|    1|     assert!(y < 10);\
+  44|     | }\
diff --git a/tests/coverage/overflow-failure/expected b/tests/coverage/overflow-failure/expected
index db4f29d51336..acba327e1d7a 100644
--- a/tests/coverage/overflow-failure/expected
+++ b/tests/coverage/overflow-failure/expected
@@ -1,9 +1,15 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks that Kani reports the correct coverage results in the case of an\
+   5|     | //! arithmetic overflow failure (caused by the second call to `cond_reduce`).\
+   6|     | \
+   7|    1| fn cond_reduce(thresh: u32, x: u32) -> u32 {\
+   8|    1|     if x > thresh { x - 50 } else { ```x''' }\
+   9|     | }\
+  10|     | \
+  11|     | #[kani::proof]\
+  12|    1| fn main() {\
+  13|    1|     cond_reduce(60, 70);\
+  14|    1|     cond_reduce(40, 42);\
+  15|     | }\
diff --git a/tests/coverage/overflow-full-coverage/expected b/tests/coverage/overflow-full-coverage/expected
index 4d17761505eb..4daa50db8510 100644
--- a/tests/coverage/overflow-full-coverage/expected
+++ b/tests/coverage/overflow-full-coverage/expected
@@ -1,9 +1,17 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks that Kani reports all regions as `COVERED` as expected in this case\
+   5|     | //! where arithmetic overflow failures are prevented.\
+   6|     | \
+   7|    1| fn reduce(x: u32) -> u32 {\
+   8|    1|     if x > 1000 { x - 1000 } else { x }\
+   9|     | }\
+  10|     | \
+  11|     | #[kani::proof]\
+  12|    1| fn main() {\
+  13|    1|     reduce(7);\
+  14|    1|     reduce(33);\
+  15|    1|     reduce(728);\
+  16|    1|     reduce(1079);\
+  17|     | }\
diff --git a/tests/coverage/while-loop-break/expected b/tests/coverage/while-loop-break/expected
index 34afef9ee12c..4e52fc5804e7 100644
--- a/tests/coverage/while-loop-break/expected
+++ b/tests/coverage/while-loop-break/expected
@@ -1,13 +1,23 @@
-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
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | \
+   4|     | //! Checks coverage results in an example with a `while` loop that returns before\
+   5|     | //! running the last iteration.\
+   6|     | \
+   7|    1| fn find_first_negative(nums: &[i32]) -> Option<i32> {\
+   8|    1|     let mut index = 0;\
+   9|    1|     while index < nums.len() {\
+  10|    1|         if nums[index] < 0 {\
+  11|    1|             return Some(nums[index]);\
+  12|    1|         }\
+  13|    1|         index += 1;\
+  14|     |     }\
+  15|    0|     ```None'''\
+  16|     | }\
+  17|     | \
+  18|     | #[kani::proof]\
+  19|    1| fn main() {\
+  20|    1|     let numbers = [1, 2, -3, 4, -5];\
+  21|    1|     let result = find_first_negative(&numbers);\
+  22|    1|     assert_eq!(result, Some(-3));\
+  23|     | }\
diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index 6e6425d086c3..1622dc104919 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -441,8 +441,11 @@ impl<'test> TestCx<'test> {
     /// Runs Kani in coverage mode on the test file specified by `self.testpaths.file`.
     fn run_expected_coverage_test(&self) {
         let proc_res = self.run_kani_with_coverage();
+        let cov_results_path = self.extract_cov_results_path(&proc_res);
+        let (kanimap, kaniraws, kanicov) = self.find_cov_files(&cov_results_path);
+        let kanicov_proc = self.run_kanicov_report(&kanimap, &kaniraws, &kanicov);
         let expected_path = self.testpaths.file.parent().unwrap().join("expected");
-        self.verify_output(&proc_res, &expected_path);
+        self.verify_output(&kanicov_proc, &expected_path);
     }
 
     /// Runs Kani with stub implementations of various data structures.
@@ -536,11 +539,88 @@ impl<'test> TestCx<'test> {
         let stamp = crate::stamp(self.config, self.testpaths);
         fs::write(stamp, "we only support one configuration").unwrap();
     }
+
+    /// Run `kani-cov merge` and `kani-cov report` to generate a text-based
+    /// report and return the `ProcRes` associated to the `kani-cov report`
+    /// command.
+    fn run_kanicov_report(
+        &self,
+        kanimap: &PathBuf,
+        kaniraws: &[PathBuf],
+        kanicov: &PathBuf,
+    ) -> ProcRes {
+        let mut kanicov_merge = Command::new("kani-cov");
+        kanicov_merge.arg("merge");
+        kanicov_merge.args(kaniraws);
+        kanicov_merge.arg("--output");
+        kanicov_merge.arg(kanicov);
+        let merge_cmd = self.compose_and_run(kanicov_merge);
+
+        if !merge_cmd.status.success() {
+            self.fatal_proc_rec("test failed: could not run `kani-cov merge` command", &merge_cmd);
+        }
+
+        let mut kanicov_report = Command::new("kani-cov");
+        kanicov_report.arg("report").arg(kanimap).arg("--profile").arg(kanicov);
+        let report_cmd = self.compose_and_run(kanicov_report);
+
+        if !report_cmd.status.success() {
+            self.fatal_proc_rec(
+                "test failed: could not run `kani-cov report` command",
+                &report_cmd,
+            );
+        }
+        report_cmd
+    }
+
+    /// Return the paths to the files to be used for the `kani-cov` commands.
+    /// Note that `kanimap` and `kaniraws` result from any coverage-enabled Kani
+    /// run. `kanicov` is the name we will use for the output of the `kani-cov
+    /// merge` command.
+    fn find_cov_files(&self, folder_path: &Path) -> (PathBuf, Vec<PathBuf>, PathBuf) {
+        let folder_name = folder_path.file_name().unwrap();
+
+        let kanimap = folder_path.join(format!("{}_kanimap.json", folder_name.to_string_lossy()));
+        let kanicov = folder_path.join(format!("{}_kanicov.json", folder_name.to_string_lossy()));
+
+        let kaniraw_glob = format!("{}/*_kaniraw.json", folder_path.display());
+        let kaniraws: Vec<PathBuf> = glob::glob(&kaniraw_glob)
+            .expect("Failed to read glob pattern")
+            .filter_map(|entry| entry.ok())
+            .collect();
+
+        (kanimap, kaniraws, kanicov)
+    }
+
+    /// Find the path to the folder where the coverage results have been saved.
+    ///
+    /// The path is displayed in the output of a coverage-enabled Kani run like
+    /// this:
+    /// ```sh
+    /// Verification Time: XX.XXXXXXXs
+    ///
+    /// [info] Coverage results saved to /path/to/cov/results/kanicov_<date>_<time>
+    /// Summary:
+    /// ```
+    fn extract_cov_results_path(&self, proc_res: &ProcRes) -> PathBuf {
+        let output_lines = proc_res.stdout.split('\n').collect::<Vec<&str>>();
+        let coverage_info = output_lines.iter().find(|l| l.contains("Coverage results saved to"));
+        if coverage_info.is_none() {
+            self.fatal_proc_rec("failed to find the path to the coverage results", proc_res);
+        }
+        let coverage_path = coverage_info
+            .unwrap()
+            .split(' ')
+            .last()
+            .expect("couldn't retrieve path to the coverage results");
+        PathBuf::from(coverage_path)
+    }
 }
 
+/// Represents the result of executing the process `cmdline`
 pub struct ProcRes {
     status: ExitStatus,
-    stdout: String,
+    pub stdout: String,
     stderr: String,
     cmdline: String,
 }
diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml
new file mode 100644
index 000000000000..4b9f14cc3ca9
--- /dev/null
+++ b/tools/kani-cov/Cargo.toml
@@ -0,0 +1,21 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "kani-cov"
+version = "0.1.0"
+edition = "2021"
+license = "MIT OR Apache-2.0"
+description = "A tool to process coverage information from Kani"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+anyhow = "1.0.81"
+clap = { version = "4.4.11", features = ["derive"] }
+console = "0.15.8"
+serde = "1.0.197"
+serde_derive = "1.0.197"
+serde_json = "1.0.115"
+tree-sitter = "0.23.0"
+tree-sitter-rust = "0.21.2"
diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs
new file mode 100644
index 000000000000..c83b3516f388
--- /dev/null
+++ b/tools/kani-cov/src/args.rs
@@ -0,0 +1,140 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module defines the data structures and validation logic for subcommands
+//! and general arguments. Most of the implementation is done through clap.
+//!
+//! Note: Validation for subcommand-specific arguments is done in the module
+//! associated with each subcommand.
+
+use std::path::PathBuf;
+
+use anyhow::{Result, bail};
+use clap::{arg, command};
+
+use crate::{merge, report, summary};
+
+/// We define three subcommands:
+///  * `merge` for merging raw Kani coverage results (AKA "kaniraw" files)
+///  * `summary` for producing a summary containing coverage metrics
+///  * `report` for generating human-readable coverage reports
+///
+/// As an example, let's assume we execute Kani with coverage enabled
+/// ```sh
+/// kani main.rs --coverage -Zsource-coverage
+/// ```
+/// the raw coverage results will be saved to a folder
+/// ```sh
+/// [info] Coverage results saved to /absolute/path/to/results/kanicov_2024-09-23_23-49
+/// ```
+///
+/// We can aggregate those results with the `merge` subcommand
+/// ```sh
+/// kani-cov merge kanicov_2024-09-23_23-49/*kaniraw.json
+/// ```
+/// which by default produces a `default_kanicov.json` file.
+///
+/// Once we have both the "kanicov" file and the "kanimap" file, we are ready to
+/// produce coverage metrics with the `summary` subcommand:
+/// ```sh
+/// kani-cov summary kanicov_2024-09-23_23-49/kanicov_2024-09-23_23-49_kanimap.json --profile default_kanicov.json
+/// ```
+///
+/// We can also produce coverage reports with the `report` subcommand:
+/// ```sh
+/// kani-cov report kanicov_2024-09-23_23-49/kanicov_2024-09-23_23-49_kanimap.json --profile default_kanicov.json
+/// ```
+#[derive(Debug, clap::Subcommand)]
+pub enum Subcommand {
+    Merge(MergeArgs),
+    Summary(SummaryArgs),
+    Report(ReportArgs),
+}
+
+/// The main command.
+/// Note: We use the same options as in Kani so that their option-parsing
+/// behaviors (and issues due to them) are as similar as possible.
+#[derive(Debug, clap::Parser)]
+#[command(
+    version,
+    name = "kani-cov",
+    about = "A tool to process coverage information from Kani",
+    args_override_self = true,
+    subcommand_negates_reqs = true,
+    subcommand_precedence_over_arg = true,
+    args_conflicts_with_subcommands = true
+)]
+pub struct Args {
+    #[command(subcommand)]
+    pub command: Option<Subcommand>,
+}
+
+/// Arguments for the `merge` subcommand
+#[derive(Debug, clap::Args)]
+pub struct MergeArgs {
+    #[arg(long)]
+    pub output: Option<PathBuf>,
+    #[arg(required = true)]
+    pub files: Vec<PathBuf>,
+}
+
+/// Arguments for the `summary` subcommand
+#[derive(Debug, clap::Args)]
+pub struct SummaryArgs {
+    // The path to the "kanimap" file
+    #[arg(required = true)]
+    pub mapfile: PathBuf,
+    // The path to the "kanicov" file
+    #[arg(long, required = true)]
+    pub profile: PathBuf,
+    // The format of the summary
+    #[arg(long, short, value_parser = clap::value_parser!(SummaryFormat), default_value = "markdown")]
+    pub format: SummaryFormat,
+}
+
+/// The format of the summary.
+///
+/// The default format is Markdown, but the CSV and JSON formats would be really
+/// nice to have.
+#[derive(Clone, Debug, PartialEq, Eq, clap::ValueEnum)]
+pub enum SummaryFormat {
+    Markdown,
+    // Csv,
+    // Json,
+}
+
+/// Arguments for the `report` subcommand
+#[derive(Debug, clap::Args)]
+pub struct ReportArgs {
+    // The path to the "kanimap" file
+    #[arg(required = true)]
+    pub mapfile: PathBuf,
+    // The path to the "kanicov" file
+    #[arg(long, required = true)]
+    pub profile: PathBuf,
+    // The format of the report
+    #[arg(long, short, value_parser = clap::value_parser!(ReportFormat), default_value = "terminal")]
+    pub format: ReportFormat,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq, clap::ValueEnum)]
+pub enum ReportFormat {
+    Terminal,
+    Escapes,
+}
+
+/// Validate general arguments and delegate validation of command-specific
+/// arguments.
+pub fn validate_args(args: &Args) -> Result<()> {
+    if args.command.is_none() {
+        bail!("subcommand needs to be specified (`merge`, `summary` or `report`)")
+    }
+
+    match args.command.as_ref().unwrap() {
+        Subcommand::Merge(merge_args) => merge::validate_merge_args(&merge_args)?,
+        Subcommand::Summary(summary_args) => summary::validate_summary_args(&summary_args)?,
+        Subcommand::Report(report_args) => report::validate_report_args(&report_args)?,
+    };
+
+    Ok(())
+}
diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs
new file mode 100644
index 000000000000..96a3dfdb7353
--- /dev/null
+++ b/tools/kani-cov/src/coverage.rs
@@ -0,0 +1,210 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module defines coverage-oriented data structures shared among
+//! subcommands and other utilities like the Rust tree-sitter.
+
+use console::style;
+use serde_derive::{Deserialize, Serialize};
+use std::path::{Path, PathBuf};
+use std::{collections::HashMap, fmt::Display};
+use std::{fmt, fs};
+use tree_sitter::{Node, Parser};
+
+pub type Function = String;
+pub type Filename = String;
+pub type LineNumber = usize;
+pub type ColumnNumber = usize;
+
+pub type LineResults = Vec<(LineNumber, Option<(usize, MarkerInfo)>)>;
+
+/// The possible outcomes for a Kani check.
+///
+/// Note: This data structure should not be duplicated in Kani -
+/// <https://github.com/model-checking/kani/issues/3541>
+#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
+#[serde(rename_all = "UPPERCASE")]
+pub enum CheckStatus {
+    Failure,
+    Covered,   // for `code_coverage` properties only
+    Satisfied, // for `cover` properties only
+    Success,
+    Undetermined,
+    Unreachable,
+    Uncovered,     // for `code_coverage` properties only
+    Unsatisfiable, // for `cover` properties only
+}
+
+/// Kani coverage check.
+///
+/// Note: This data structure should not be duplicated in Kani -
+/// <https://github.com/model-checking/kani/issues/3541>
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct CoverageCheck {
+    pub function: Filename,
+    term: CoverageTerm,
+    pub region: CoverageRegion,
+    pub status: CheckStatus,
+}
+
+// Note: This `impl` should not be duplicated in Kani -
+// <https://github.com/model-checking/kani/issues/3541>
+impl std::fmt::Display for CheckStatus {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let check_str = match self {
+            CheckStatus::Satisfied => style("SATISFIED").green(),
+            CheckStatus::Success => style("SUCCESS").green(),
+            CheckStatus::Covered => style("COVERED").green(),
+            CheckStatus::Uncovered => style("UNCOVERED").red(),
+            CheckStatus::Failure => style("FAILURE").red(),
+            CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
+            CheckStatus::Undetermined => style("UNDETERMINED").yellow(),
+            CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(),
+        };
+        write!(f, "{check_str}")
+    }
+}
+
+/// Raw Kani coverage results.
+///
+/// Note: This data structure should not be duplicated in Kani -
+/// <https://github.com/model-checking/kani/issues/3541>
+#[derive(Clone, Debug, Serialize, Deserialize)]
+pub struct CoverageResults {
+    pub data: HashMap<Function, Vec<CoverageCheck>>,
+}
+
+/// Aggregated coverage results.
+#[derive(Clone, Debug, Serialize, Deserialize)]
+pub struct CombinedCoverageResults {
+    pub data: HashMap<Filename, Vec<(Function, Vec<CovResult>)>>,
+}
+
+/// The coverage result associated to a particular coverage region.
+///
+/// Basically, this aggregates the information of one or more `CoverageCheck`
+/// for a particular region. Thus, `total_times` represents the total number of
+/// such checks, while `times_covered` keeps track of how many of those checks
+/// had the `COVERED` status.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct CovResult {
+    pub function: Filename,
+    pub region: CoverageRegion,
+    pub times_covered: usize,
+    pub total_times: usize,
+}
+
+/// A coverage region.
+/// `start` and `end` are tuples containing the line and column numbers.
+///
+/// Note: This data structure should not be duplicated in Kani -
+/// <https://github.com/model-checking/kani/issues/3541>
+#[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)]
+pub struct CoverageRegion {
+    pub file: Filename,
+    pub start: (LineNumber, ColumnNumber),
+    pub end: (LineNumber, ColumnNumber),
+}
+
+impl Display for CoverageRegion {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}:{}:{} - {}:{}", self.file, self.start.0, self.start.1, self.end.0, self.end.1)
+    }
+}
+
+/// A coverage term.
+///
+/// Note: This data structure should not be duplicated in Kani -
+/// <https://github.com/model-checking/kani/issues/3541>
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub enum CoverageTerm {
+    Counter(u32),
+    Expression(u32),
+}
+
+/// The coverage information to produce for a particular file.
+pub struct FileCoverageInfo {
+    pub filename: Filename,
+    pub function: CoverageMetric,
+    pub line: CoverageMetric,
+    pub region: CoverageMetric,
+}
+
+/// A coverage metric.
+pub struct CoverageMetric {
+    pub covered: usize,
+    pub total: usize,
+}
+
+impl CoverageMetric {
+    pub fn new(covered: usize, total: usize) -> Self {
+        CoverageMetric { covered, total }
+    }
+}
+
+/// Function information obtained through a tree-sitter
+#[derive(Debug)]
+pub struct FunctionInfo {
+    pub name: Function,
+    pub start: (LineNumber, ColumnNumber),
+    pub end: (LineNumber, ColumnNumber),
+}
+
+/// Extract function information from a file using a tree-sitter
+pub fn function_info_from_file(filepath: &PathBuf) -> Vec<FunctionInfo> {
+    let source_code = fs::read_to_string(filepath).expect("could not read source file");
+    let mut parser = Parser::new();
+    parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar");
+
+    let tree = parser.parse(&source_code, None).expect("Failed to parse file");
+
+    let source_code_bytes = source_code.as_bytes();
+    let mut function_info: Vec<FunctionInfo> = Vec::new();
+    let mut cursor = tree.walk();
+
+    for node in tree.root_node().children(&mut cursor) {
+        if node.kind() == "function_item" {
+            function_info.push(function_info_from_node(node, source_code_bytes));
+        }
+    }
+
+    function_info
+}
+
+/// Helper function to extract function information using a tree-sitter
+fn function_info_from_node(node: Node, source: &[u8]) -> FunctionInfo {
+    let name = node
+        .child_by_field_name("name")
+        .and_then(|name| name.utf8_text(source).ok())
+        .expect("couldn't get function name")
+        .to_string();
+    let start = (node.start_position().row + 1, node.start_position().column + 1);
+    let end = (node.end_position().row + 1, node.end_position().column + 1);
+    FunctionInfo { name, start, end }
+}
+
+/// Extract the coverage results associated to a function
+pub fn function_coverage_results(
+    info: &FunctionInfo,
+    file: &Path,
+    results: &CombinedCoverageResults,
+) -> Option<(Function, Vec<CovResult>)> {
+    // The filenames in "kaniraw" files are not absolute, so we need to match
+    // them with the ones we have in the aggregated results (i.e., the filenames
+    // in the "kanimap" files).
+    let filename = file.to_str()?;
+    let right_filename = results.data.keys().find(|p| filename.ends_with(*p)).unwrap();
+    // TODO: The filenames in kaniraw files should be absolute, just like in metadata.
+    // Otherwise the key for `results` just fails... <https://github.com/model-checking/kani/issues/3542>
+    let file_results = results.data.get(right_filename).unwrap();
+    let function = &info.name;
+    let fun_results = file_results.iter().find(|(f, _)| *f == *function);
+    fun_results.cloned()
+}
+
+/// Marker information, mainly useful for highlighting coverage
+#[derive(Debug, Clone)]
+pub enum MarkerInfo {
+    FullLine,
+    Markers(Vec<CovResult>),
+}
diff --git a/tools/kani-cov/src/main.rs b/tools/kani-cov/src/main.rs
new file mode 100644
index 000000000000..438d2bc91394
--- /dev/null
+++ b/tools/kani-cov/src/main.rs
@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Main module of `kani-cov`, containing its main function.
+
+mod args;
+mod coverage;
+mod merge;
+mod report;
+mod summary;
+
+use anyhow::Result;
+use args::{Subcommand, validate_args};
+use clap::Parser;
+
+/// The main function of `kani-cov`.
+/// First, we parse and validate the subcommand and arguments. Then, we call the
+/// main function for the subcommand that had been specified.
+fn main() -> Result<()> {
+    let args = args::Args::parse();
+
+    validate_args(&args)?;
+
+    match args.command.unwrap() {
+        Subcommand::Merge(merge_args) => merge::merge_main(&merge_args)?,
+        Subcommand::Summary(summary_args) => summary::summary_main(&summary_args)?,
+        Subcommand::Report(report_args) => report::report_main(&report_args)?,
+    };
+
+    Ok(())
+}
diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs
new file mode 100644
index 000000000000..2e8452393fb0
--- /dev/null
+++ b/tools/kani-cov/src/merge.rs
@@ -0,0 +1,145 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module includes the implementation of the `merge` subcommand.
+
+use std::{
+    collections::{HashMap, HashSet},
+    fs::{File, OpenOptions},
+    io::{BufReader, BufWriter},
+    path::PathBuf,
+};
+
+use anyhow::Result;
+
+use crate::{
+    args::MergeArgs,
+    coverage::{
+        CheckStatus, CombinedCoverageResults, CovResult, CoverageCheck, CoverageResults, Filename,
+        Function,
+    },
+};
+
+/// Executes the `merge` subcommand.
+///
+/// First, it loads the raw coverage results from "kaniraw" files. Then, it
+/// combines those results by coverage region thereby producing aggregated
+/// coverage information. Finally, it saves that information into another file
+/// (the coverage profile also known as the "kanicov" file).
+pub fn merge_main(args: &MergeArgs) -> Result<()> {
+    let raw_results = parse_raw_results(&args.files)?;
+    let combined_results = combine_raw_results(&raw_results);
+    save_combined_results(&combined_results, &args.output)?;
+    Ok(())
+}
+
+/// Validate arguments to the `merge` subcommand in addition to clap's
+/// validation.
+pub fn validate_merge_args(_args: &MergeArgs) -> Result<()> {
+    // No validation is done at the moment
+    Ok(())
+}
+
+/// Parse raw coverage results from a set of files (AKA "kaniraw" files)
+fn parse_raw_results(paths: &Vec<PathBuf>) -> Result<Vec<CoverageResults>> {
+    let mut raw_results = Vec::with_capacity(paths.len());
+    for path in paths {
+        let filename = path.to_string_lossy();
+        let file = File::open(path).expect(&format!("could not open file {filename}"));
+        let reader = BufReader::new(file);
+
+        let result = serde_json::from_reader(reader)
+            .expect(&format!("could not deserialize file {filename}"));
+        raw_results.push(result);
+    }
+    Ok(raw_results)
+}
+
+/// Combine raw coverage results into an aggregated form
+fn combine_raw_results(results: &Vec<CoverageResults>) -> CombinedCoverageResults {
+    let all_file_function_names = function_names_from_results(results);
+
+    let mut new_data: HashMap<Filename, Vec<(Function, Vec<CovResult>)>> = HashMap::new();
+
+    for (file_name, fun_name) in all_file_function_names {
+        let mut this_fun_checks: Vec<&CoverageCheck> = Vec::new();
+
+        for result in results {
+            if result.data.contains_key(&file_name) {
+                this_fun_checks.extend(
+                    result
+                        .data
+                        .get(&file_name)
+                        .unwrap()
+                        .iter()
+                        .filter(|check| check.function == fun_name),
+                )
+            }
+        }
+
+        let mut new_results = Vec::new();
+
+        while !this_fun_checks.is_empty() {
+            // Take the first check, and split `this_fun_checks` into checks
+            // covering the same region as that check, and checks which do not.
+            let this_region_check = this_fun_checks[0];
+            let (same_region_checks, other_region_checks) = this_fun_checks
+                .into_iter()
+                .partition(|check| check.region == this_region_check.region);
+            // Update `this_fun_checks` with checks that aren't being processed yet
+            this_fun_checks = other_region_checks;
+
+            // Calculate `total_times` and `times_covered` for this region
+            let total_times = same_region_checks.len();
+            let times_covered = same_region_checks
+                .iter()
+                .filter(|check| check.status == CheckStatus::Covered)
+                .count();
+
+            let new_result = CovResult {
+                function: fun_name.clone(),
+                region: this_region_check.region.clone(),
+                times_covered,
+                total_times,
+            };
+            new_results.push(new_result);
+        }
+
+        let filename_copy = file_name.clone();
+        if new_data.contains_key(&file_name) {
+            new_data.get_mut(&filename_copy).unwrap().push((fun_name, new_results));
+        } else {
+            new_data.insert(file_name.clone(), vec![(fun_name, new_results)]);
+        }
+    }
+    CombinedCoverageResults { data: new_data }
+}
+
+/// Save the combined coverage results into a file
+fn save_combined_results(
+    results: &CombinedCoverageResults,
+    output: &Option<PathBuf>,
+) -> Result<()> {
+    let output_path =
+        if let Some(out) = output { out } else { &PathBuf::from("default_kanicov.json") };
+
+    let file = OpenOptions::new().write(true).create(true).truncate(true).open(output_path)?;
+    let writer = BufWriter::new(file);
+
+    serde_json::to_writer(writer, results)?;
+
+    Ok(())
+}
+
+/// All function names appearing in raw coverage results
+fn function_names_from_results(results: &[CoverageResults]) -> Vec<(Filename, Function)> {
+    let mut file_function_pairs = HashSet::new();
+    for result in results {
+        for (file, checks) in &result.data {
+            for check in checks {
+                file_function_pairs.insert((file.clone(), check.function.clone()));
+            }
+        }
+    }
+    file_function_pairs.into_iter().collect()
+}
diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs
new file mode 100644
index 000000000000..95eba4d252ee
--- /dev/null
+++ b/tools/kani-cov/src/report.rs
@@ -0,0 +1,267 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module includes the implementation of the `report` subcommand.
+
+use std::io::{BufRead, IsTerminal};
+use std::{fs::File, io::BufReader, path::PathBuf};
+
+use anyhow::Result;
+
+use crate::args::ReportFormat;
+use crate::coverage::{
+    ColumnNumber, CovResult, LineNumber, LineResults, MarkerInfo, function_coverage_results,
+    function_info_from_file,
+};
+use crate::summary::line_coverage_results;
+use crate::{args::ReportArgs, coverage::CombinedCoverageResults};
+
+/// Executes the `report` subcommand.
+///
+/// First, it loads the coverage metadata and results from the files passed as
+/// arguments. Then, for each file referenced in the metadata, it computes its
+/// associated coverage information on a per-function basis, producing a
+/// human-readable report for each one of the files.
+pub fn report_main(args: &ReportArgs) -> Result<()> {
+    let mapfile = File::open(&args.mapfile)?;
+    let reader = BufReader::new(mapfile);
+
+    let covfile = File::open(&args.profile)?;
+    let covreader = BufReader::new(covfile);
+    let results: CombinedCoverageResults =
+        serde_json::from_reader(covreader).expect("could not load coverage results");
+
+    let source_files: Vec<PathBuf> =
+        serde_json::from_reader(reader).expect("could not parse coverage metadata");
+
+    let checked_format = check_format(&args.format);
+
+    for file in source_files {
+        let fun_info = function_info_from_file(&file);
+        let mut file_cov_info = Vec::new();
+        for info in fun_info {
+            let cov_results = function_coverage_results(&info, &file, &results);
+            let line_coverage = line_coverage_results(&info, &cov_results);
+            let line_coverage_matched: LineResults =
+                (info.start.0..=info.end.0).zip(line_coverage.clone()).collect();
+            file_cov_info.push(line_coverage_matched);
+        }
+        output_coverage_results(&checked_format, file, file_cov_info)?;
+    }
+
+    Ok(())
+}
+
+/// Validate arguments to the `report` subcommand in addition to clap's
+/// validation.
+pub fn validate_report_args(_args: &ReportArgs) -> Result<()> {
+    // No validation is done at the moment
+    Ok(())
+}
+
+/// Checks the `format` argument for the `report` subcommand and selects to
+/// another format if the one we are checking is not possible for any reason.
+///
+/// For example, if the `Terminal` format is specified but we are not writing to
+/// a terminal, it will auto-select the `Escapes` format to avoid character
+/// issues.
+fn check_format(format: &ReportFormat) -> ReportFormat {
+    let is_terminal = std::io::stdout().is_terminal();
+    match format {
+        ReportFormat::Terminal => {
+            if is_terminal {
+                ReportFormat::Terminal
+            } else {
+                ReportFormat::Escapes
+            }
+        }
+        ReportFormat::Escapes => ReportFormat::Escapes,
+    }
+}
+
+/// Output coverage results, and highlight regions or lines which are not
+/// covered.
+///
+/// When highlighting the terminal, highlighted areas must be closed on the each
+/// line to avoid highlighting beyond the source code area. Therefore, this
+/// highlighting algorithm emits codes for both opening and closing the
+/// highlighted area if any highlighting must be done for a line.
+///
+/// Therefore, a coverage region spanning multiple lines will be represented
+/// with multiple highlighted lines. For example, let's take this uncovered
+/// function:
+///
+/// fn _other_function() {
+///     println!("Hello, world!");
+/// }
+///
+/// It will be highlighted as follows:
+///
+/// ```fn _other_function() {'''
+/// ```    println!("Hello, world!");'''
+/// ```}'''
+///
+/// Note how there is always a corresponding escape for each line.
+/// This is more sophisticated than the naive solution, which would simply emit two escapes
+/// per region (one opening, one closing) as follows:
+///
+/// ```fn _other_function() {
+///     println!("Hello, world!");
+/// }'''
+///
+pub fn output_coverage_results(
+    format: &ReportFormat,
+    filepath: PathBuf,
+    results: Vec<LineResults>,
+) -> Result<()> {
+    let flattened_results: LineResults = results.into_iter().flatten().collect();
+    println!("{}", filepath.to_string_lossy());
+
+    let file = File::open(filepath)?;
+    let reader = BufReader::new(file);
+
+    let mut must_highlight = false;
+
+    for (i, line) in reader.lines().enumerate() {
+        let idx = i + 1;
+        let line = line?;
+
+        let cur_line_result = flattened_results.iter().find(|(num, _)| *num == idx);
+
+        let (max_times, line_fmt) = if let Some((_, Some((max, marker_info)))) = cur_line_result {
+            match marker_info {
+                MarkerInfo::FullLine => {
+                    (Some(max), insert_escapes(&line, vec![(0, true), (line.len(), false)], format))
+                }
+                MarkerInfo::Markers(results) => {
+                    // Escapes for the regions which start and finish in this line
+                    let complete_escapes: Vec<(ColumnNumber, bool)> = results
+                        .iter()
+                        .filter(|m| {
+                            m.times_covered == 0 && m.region.start.0 == idx && m.region.end.0 == idx
+                        })
+                        .flat_map(|m| {
+                            vec![((m.region.start.1 - 1), true), ((m.region.end.1 - 1), false)]
+                        })
+                        .collect();
+                    // Escapes for the regions which only start in this line
+                    let mut opening_escapes: Vec<(ColumnNumber, bool)> = results
+                        .iter()
+                        .filter(|m| {
+                            m.times_covered == 0 && m.region.start.0 == idx && m.region.end.0 != idx
+                        })
+                        .flat_map(|m| vec![((m.region.start.1 - 1), true)])
+                        .collect();
+                    // Escapes for the regions which only finish in this line
+                    let mut closing_escapes: Vec<(ColumnNumber, bool)> = results
+                        .iter()
+                        .filter(|m| {
+                            m.times_covered == 0 && m.region.start.0 != idx && m.region.end.0 == idx
+                        })
+                        .flat_map(|m| vec![((m.region.end.1 - 1), false)])
+                        .collect();
+
+                    // Emit an opening escape if there was a closing one and we
+                    // had to continue the highlight
+                    if must_highlight && !closing_escapes.is_empty() {
+                        closing_escapes.push((0, true));
+                        must_highlight = false;
+                    }
+                    // Continue the highlight in the next lines if we had an
+                    // opening escape
+                    if !opening_escapes.is_empty() {
+                        opening_escapes.push((line.len(), false));
+                        must_highlight = true;
+                    }
+
+                    // Join all the escapes, then insert them
+                    closing_escapes.extend(complete_escapes);
+                    closing_escapes.extend(opening_escapes);
+
+                    if must_highlight && closing_escapes.is_empty() {
+                        closing_escapes.push((0, true));
+                        closing_escapes.push((line.len(), false));
+                    }
+
+                    // If any result points to an out-of-bounds region after the
+                    // end of the line (due to a known issue), we extend the
+                    // line with a space to avoid crashing when drawing it.
+                    let line = if results_with_nonexisting_regions_in_line(results, &line, idx) {
+                        format!("{line} ")
+                    } else {
+                        line
+                    };
+
+                    (Some(max), insert_escapes(&line, closing_escapes, format))
+                }
+            }
+        } else {
+            (
+                None,
+                if !must_highlight {
+                    line
+                } else {
+                    insert_escapes(&line, vec![(0, true), (line.len(), false)], format)
+                },
+            )
+        };
+
+        let max_fmt =
+            if let Some(num) = max_times { format!("{num:4}") } else { format!("{:4}", " ") };
+
+        println!("{idx:4}| {max_fmt}| {line_fmt}");
+    }
+
+    Ok(())
+}
+
+/// Returns whether any of the coverage results for a line point to out-of-bound
+/// regions.
+///
+/// This is helpful to detect cases in which, for an unknown reason, the Rust
+/// coverage instrumentation inserts a single-column code span after the end of
+/// a line. More details in <https://github.com/model-checking/kani/issues/3543>
+fn results_with_nonexisting_regions_in_line(
+    results: &[CovResult],
+    line: &str,
+    idx: LineNumber,
+) -> bool {
+    let results_with_oob_regions = results.iter().filter(|m| {
+        m.region.start.0 == idx
+            && m.region.end.0 == idx
+            && (m.region.end.1 - m.region.start.1 == 1)
+            && (m.region.end.1) > line.len()
+    });
+    results_with_oob_regions.count() > 0
+}
+
+/// Inserts opening/closing escape strings into `str` given a set of `markers`.
+/// Each marker is a tuple `(offset, type)` where:
+///  * `offset` represents the offset in which the marker must be inserted, and
+///  * `type` represents whether it is an opening (`true`) or closing (`false`)
+///    escape.
+///
+/// The specific escape to be used are determined by the report format.
+fn insert_escapes(str: &str, markers: Vec<(ColumnNumber, bool)>, format: &ReportFormat) -> String {
+    // Determine the escape strings based on the format
+    let (open_escape, close_escape) = match format {
+        ReportFormat::Terminal => ("\x1b[41m", "\x1b[0m"),
+        ReportFormat::Escapes => ("```", "'''"),
+    };
+
+    let mut escape_markers: Vec<(&ColumnNumber, &str)> =
+        markers.iter().map(|(i, b)| (i, if *b { open_escape } else { close_escape })).collect();
+    escape_markers.sort();
+
+    let mut escaped_str = str.to_owned();
+    let mut offset = 0;
+
+    // Iteratively insert the escape strings into the original string
+    for (i, b) in escape_markers {
+        escaped_str.insert_str(i + offset, b);
+        // `offset` keeps track of the bytes we've already inserted so the original
+        // index is shifted by the appropriate amount in subsequent insertions.
+        offset += b.bytes().len();
+    }
+    escaped_str
+}
diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs
new file mode 100644
index 000000000000..e56008daade1
--- /dev/null
+++ b/tools/kani-cov/src/summary.rs
@@ -0,0 +1,300 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module includes the implementation of the `summary` subcommand.
+
+use std::{
+    cmp::max,
+    fs::File,
+    io::BufReader,
+    path::{Path, PathBuf},
+};
+
+use anyhow::Result;
+
+use crate::{
+    args::{SummaryArgs, SummaryFormat},
+    coverage::{
+        CombinedCoverageResults, CovResult, CoverageMetric, CoverageRegion, FileCoverageInfo,
+        Function, FunctionInfo, LineNumber, MarkerInfo, function_coverage_results,
+        function_info_from_file,
+    },
+};
+
+/// Executes the `summary` subcommand.
+///
+/// First, it loads the coverage metadata and results from the files passed as
+/// arguments. Then, for each file referenced in the metadata, it computes its
+/// associated coverage information on a per-function basis, producing coverage
+/// metrics for each one of the files.
+pub fn summary_main(args: &SummaryArgs) -> Result<()> {
+    let mapfile = File::open(&args.mapfile)?;
+    let reader = BufReader::new(mapfile);
+
+    let covfile = File::open(&args.profile)?;
+    let covreader = BufReader::new(covfile);
+    let results: CombinedCoverageResults =
+        serde_json::from_reader(covreader).expect("could not load coverage results");
+
+    let source_files: Vec<PathBuf> =
+        serde_json::from_reader(reader).expect("could not parse coverage metadata");
+
+    let mut all_cov_info: Vec<FileCoverageInfo> = Vec::new();
+
+    for file in source_files {
+        let fun_info = function_info_from_file(&file);
+        let mut file_cov_info = Vec::new();
+        for info in fun_info {
+            let cov_results = function_coverage_results(&info, &file, &results);
+            let function_coverage = function_coverage_info(&cov_results);
+            let line_coverage = line_coverage_info(&info, &cov_results);
+            let region_coverage = region_coverage_info(&cov_results);
+            let cur_function_coverage_results = FunctionCoverageResults {
+                is_covered: function_coverage,
+                total_lines: line_coverage.1,
+                covered_lines: line_coverage.0,
+                covered_regions: region_coverage.0,
+                total_regions: region_coverage.1,
+            };
+            file_cov_info.push(cur_function_coverage_results);
+        }
+        let aggr_cov_info = calculate_cov_info(&file, &file_cov_info);
+        all_cov_info.push(aggr_cov_info);
+    }
+    print_coverage_info(&all_cov_info, &args.format);
+
+    Ok(())
+}
+
+/// Calculate the coverage information (metrics) for a file
+fn calculate_cov_info(file: &Path, file_cov_info: &[FunctionCoverageResults]) -> FileCoverageInfo {
+    let total_functions = file_cov_info.len();
+    let covered_functions = file_cov_info.iter().filter(|f| f.is_covered).count();
+    let fun_cov_info = CoverageMetric::new(covered_functions, total_functions);
+
+    let covered_lines = file_cov_info.iter().map(|c| c.covered_lines).sum();
+    let total_lines = file_cov_info.iter().map(|c| c.total_lines).sum();
+    let lines_cov_info = CoverageMetric::new(covered_lines, total_lines);
+
+    let covered_regions = file_cov_info.iter().map(|c| c.covered_regions).sum();
+    let total_regions = file_cov_info.iter().map(|c| c.total_regions).sum();
+    let region_cov_info = CoverageMetric::new(covered_regions, total_regions);
+
+    FileCoverageInfo {
+        filename: file.to_string_lossy().to_string(),
+        function: fun_cov_info,
+        line: lines_cov_info,
+        region: region_cov_info,
+    }
+}
+
+fn function_coverage_info(cov_results: &Option<(Function, Vec<CovResult>)>) -> bool {
+    if let Some(res) = cov_results { res.1.iter().any(|c| c.times_covered > 0) } else { false }
+}
+
+/// Function coverage results
+struct FunctionCoverageResults {
+    is_covered: bool,
+    covered_lines: usize,
+    total_lines: usize,
+    covered_regions: usize,
+    total_regions: usize,
+}
+
+/// Validate arguments to the `summary` subcommand in addition to clap's
+/// validation.
+pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> {
+    // No validation is done at the moment
+    Ok(())
+}
+
+/// Computes coverage results from a line-based perspective.
+///
+/// Basically, for each line we produce an `<Option<(usize, MarkerInfo)>>`
+/// result where:
+///  * `None` means there were no coverage results associated with this line.
+///    This may happen in lines that only contain a closing `}`, for example.
+///  * `Some(max, markers)` means there were coverage results associated with
+///    the line or we deduced no results were possible based on function
+///    information (i.e., the function was not reachable during verification).
+///    Here, `max` represents the maximum number of times the line was covered by
+///    any coverage result, and `markers` represents marker information which is
+///    relevant to the line (including coverage results).
+///
+/// As a result, we essentially precompute here most of the information required
+/// for the generation of coverage reports.
+pub fn line_coverage_results(
+    info: &FunctionInfo,
+    fun_results: &Option<(Function, Vec<CovResult>)>,
+) -> Vec<Option<(usize, MarkerInfo)>> {
+    let start_line = info.start.0;
+    let end_line = info.end.0;
+
+    let mut line_status: Vec<Option<(usize, MarkerInfo)>> =
+        Vec::with_capacity(end_line - start_line + 1);
+
+    if let Some(res) = fun_results {
+        let mut cur_results = res.1.clone();
+        // Sort the results by row
+        cur_results.sort_by(|a, b| b.region.start.0.cmp(&a.region.start.0));
+
+        /// Checks if a line is relevant to a region.
+        /// Here, we define "relevant" as the line appearing after/at the start
+        /// of a region and before/at the end of a region.
+        fn line_relevant_to_region(line: LineNumber, region: &CoverageRegion) -> bool {
+            region.start.0 <= line && region.end.0 >= line
+        }
+
+        for line in start_line..end_line {
+            // Filter results which are relevant to the current line
+            let line_results: Vec<crate::coverage::CovResult> = cur_results
+                .iter()
+                .filter(|c| line_relevant_to_region(line, &c.region))
+                .cloned()
+                .collect();
+
+            if line_results.is_empty() {
+                line_status.push(None);
+            } else {
+                let max_covered = line_results
+                    .iter()
+                    .max_by_key(|res| res.times_covered)
+                    .map(|res| res.times_covered)
+                    .unwrap_or(0);
+                line_status.push(Some((max_covered, MarkerInfo::Markers(line_results))));
+            }
+        }
+    } else {
+        line_status = std::iter::repeat(Some((0, MarkerInfo::FullLine)))
+            .take(end_line - start_line + 1)
+            .collect();
+    }
+    line_status
+}
+
+/// Compute the number of covered lines and number of total lines given the
+/// coverage results for a given function.
+pub fn line_coverage_info(
+    info: &FunctionInfo,
+    fun_results: &Option<(Function, Vec<CovResult>)>,
+) -> (usize, usize) {
+    let line_status = line_coverage_results(info, fun_results);
+    let total_lines = line_status.iter().filter(|s| s.is_some()).count();
+    let covered_lines =
+        line_status.iter().filter(|s| s.is_some() && s.as_ref().unwrap().0 > 0).count();
+    (covered_lines, total_lines)
+}
+
+/// Compute the number of covered regions and number of total regions given the
+/// coverage results for a given function.
+fn region_coverage_info(fun_results: &Option<(Function, Vec<CovResult>)>) -> (usize, usize) {
+    if let Some(res) = fun_results {
+        let total_regions = res.1.len();
+        let covered_regions = res.1.iter().filter(|c| c.times_covered > 0).count();
+        (covered_regions, total_regions)
+    } else {
+        (0, 0)
+    }
+}
+
+/// Output coverage information for a set of files
+fn print_coverage_info(info: &Vec<FileCoverageInfo>, format: &SummaryFormat) {
+    match format {
+        SummaryFormat::Markdown => print_coverage_markdown_info(info),
+        // SummaryFormat::Json => print_coverage_json_info(info),
+    }
+}
+
+/// Output coverage information for a set of files in the markdown format
+fn print_coverage_markdown_info(info: &Vec<FileCoverageInfo>) {
+    fn safe_div(num: usize, denom: usize) -> Option<f32> {
+        if denom == 0 { None } else { Some(num as f32 / denom as f32) }
+    }
+
+    const HEADERS_ROWS: usize = 3;
+    const FILENAME_HEADER: &str = "Filename";
+    const FUNCTION_HEADER: &str = "Function (%)";
+    const LINE_HEADER: &str = "Line (%)";
+    const REGION_HEADER: &str = "Region (%)";
+
+    let mut table_rows: Vec<String> = Vec::with_capacity(HEADERS_ROWS + info.len() + 1);
+    let mut max_filename_fmt_width = FILENAME_HEADER.len();
+    let mut max_function_fmt_width = FUNCTION_HEADER.len();
+    let mut max_line_fmt_width = LINE_HEADER.len();
+    let mut max_region_fmt_width = REGION_HEADER.len();
+
+    let mut data_rows: Vec<(String, String, String, String)> = Vec::with_capacity(info.len());
+
+    for cov_info in info {
+        let filename = cov_info.filename.to_string();
+
+        let function_covered = cov_info.function.covered;
+        let function_total = cov_info.function.total;
+        let function_rate = safe_div(function_covered, function_total);
+        let function_rate_fmt = if let Some(rate) = function_rate {
+            format!("{:.2}", (rate * 100_f32))
+        } else {
+            "N/A".to_string()
+        };
+        let function_fmt = format!("{function_covered}/{function_total} ({function_rate_fmt})");
+
+        let line_covered = cov_info.line.covered;
+        let line_total = cov_info.line.total;
+        let line_rate = safe_div(line_covered, line_total);
+        let line_rate_fmt = if let Some(rate) = line_rate {
+            format!("{:.2}", (rate * 100_f32))
+        } else {
+            "N/A".to_string()
+        };
+        let line_fmt = format!("{line_covered}/{line_total} ({line_rate_fmt})");
+
+        let region_covered = cov_info.region.covered;
+        let region_total = cov_info.region.total;
+        let region_rate = safe_div(region_covered, region_total);
+        let region_rate_fmt = if let Some(rate) = region_rate {
+            format!("{:.2}", (rate * 100_f32))
+        } else {
+            "N/A".to_string()
+        };
+        let region_fmt = format!("{region_covered}/{region_total} ({region_rate_fmt})");
+
+        max_filename_fmt_width = max(max_filename_fmt_width, filename.len());
+        max_function_fmt_width = max(max_function_fmt_width, function_fmt.len());
+        max_line_fmt_width = max(max_line_fmt_width, line_fmt.len());
+        max_region_fmt_width = max(max_region_fmt_width, region_fmt.len());
+
+        data_rows.push((filename, function_fmt, line_fmt, region_fmt));
+    }
+
+    let filename_space = " ".repeat(max_filename_fmt_width - FILENAME_HEADER.len());
+    let function_space = " ".repeat(max_function_fmt_width - FUNCTION_HEADER.len());
+    let line_space = " ".repeat(max_line_fmt_width - LINE_HEADER.len());
+    let region_space = " ".repeat(max_region_fmt_width - REGION_HEADER.len());
+
+    let header_row = format!(
+        "| {FILENAME_HEADER}{filename_space} | {FUNCTION_HEADER}{function_space} | {LINE_HEADER}{line_space} | {REGION_HEADER}{region_space} |"
+    );
+    table_rows.push(header_row);
+
+    let filename_sep = "-".repeat(max_filename_fmt_width);
+    let function_sep = "-".repeat(max_function_fmt_width);
+    let line_sep = "-".repeat(max_line_fmt_width);
+    let region_sep = "-".repeat(max_region_fmt_width);
+
+    let sep_row = format!("| {filename_sep} | {function_sep} | {line_sep} | {region_sep} |");
+    table_rows.push(sep_row);
+
+    for (filename, function_fmt, line_fmt, region_fmt) in data_rows {
+        let filename_space = " ".repeat(max_filename_fmt_width - filename.len());
+        let function_space = " ".repeat(max_function_fmt_width - function_fmt.len());
+        let line_space = " ".repeat(max_line_fmt_width - line_fmt.len());
+        let region_space = " ".repeat(max_region_fmt_width - region_fmt.len());
+
+        let cur_row = format!(
+            "| {filename}{filename_space} | {function_fmt}{function_space} | {line_fmt}{line_space} | {region_fmt}{region_space} |"
+        );
+        table_rows.push(cur_row);
+    }
+
+    println!("{}", table_rows.join("\n"));
+}