From 5ed66ed2b39beda8cd8422c15a4b712d20d2103e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 23 Aug 2024 20:30:15 +0000 Subject: [PATCH] Complete default behavior for Kani coverage workflow --- rfc/src/rfcs/0011-source-coverage.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0011-source-coverage.md b/rfc/src/rfcs/0011-source-coverage.md index 232869a1236c..9ea23c72a9d1 100644 --- a/rfc/src/rfcs/0011-source-coverage.md +++ b/rfc/src/rfcs/0011-source-coverage.md @@ -508,7 +508,10 @@ uses the JSON format but we might consider using a binary format if it doesn't scale. In addition, Kani will produce two types of coverage results: - 1. A coverage summary + 1. A coverage summary with the default options. + 2. A terminal-based coverage report with the default options. However, we will + only do this if the program is composed of a single source + file[^note-conditional-report]. [^note-kanimap]: Note that the `.kanimap` generation isn't implemented in [#3119](https://github.com/model-checking/kani/pull/3119). The [draft @@ -517,6 +520,10 @@ In addition, Kani will produce two types of coverage results: the source files referred to by the code coverage checks, but it doesn't get information about code trimmed out by the MIR linker. +[^note-conditional-report]: In other words, standalone `kani` would always emit +these terminal-based reports, but `cargo kani` would not unless the project +contains a single Rust file (for example, `src/main.rs`). + ## Rationale and alternatives ### Other coverage implementations