"%t_coverage_reports"/coverage_tests_actual.html
+// RUN: %diff "%S/CoverageReport.dfy_tests_actual.html.expect" "%t_coverage_reports/coverage_tests_actual.html"
+
+// Manually assert the other backends cleanly report they don't support this feature yet
+// RUN: %exits-with 3 %baredafny run %args -t:java --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s > "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:js --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:go --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:py --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:cpp --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %exits-with 3 %baredafny run %args -t:rs --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "BranchCoverage.dfy"
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect
new file mode 100644
index 00000000000..050212ee153
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy.expect
@@ -0,0 +1,18 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
+
+Dafny program verifier finished with 0 verified, 0 errors
+CoverageReport.dfy(20,0): Error: Feature not supported for this compilation target: Execution coverage report
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
new file mode 100644
index 00000000000..50b452d2ad2
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect
@@ -0,0 +1,228 @@
+
+
+
+
+
+
+ BranchCoverage.dfy, Execution Coverage
+
+
+
+BranchCoverage.dfy, Execution Coverage
+
+
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:cs %S/BranchCoverage2.cs "%s" > "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:js %S/BranchCoverage3.js "%s" >> "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:go %S/BranchCoverage4.go "%s" >> "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:java %S/CodeCoverage.java "%s" >> "%t"
+// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:py %S/BranchCoverage.py "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The Main method is at the end of this file, because that makes it easier to maintain
+// this test file when adding more tests.
+
+// ---------- class constructor ----------
+
+class MyClass {
+ constructor () { // 3 times
+ }
+}
+
+// ---------- routines that are never called ----------
+
+method NeverCalled() {
+ // we get here 0 times
+}
+
+function FunctionNeverCalled(): int {
+ // we get here 0 times
+ 75
+}
+
+// ---------- if ----------
+
+method M(x: int) returns (y: int) {
+ // we get here 3 times
+ if x < 10 {
+ return x + 20; // we get here 1 time
+ } else if x < 20 { // note: the location between th "else" and the "if" does not get recorded
+ return x + 20; // we get here 0 times
+ } else {
+ return 100; // we get here 2 times
+ }
+}
+
+method N(x: int) returns (y: int) {
+ // we get here 3 times
+ y := 100;
+ if x < 10 {
+ return x + 20; // we get here 1 time
+ } else if x < 20 { // note: the location between th "else" and the "if" does not get recorded
+ return x + 20; // we get here 0 times
+ } // we get to this implicit else 2 times
+}
+
+
+method P(x: int) {
+ // we get here 1 time
+ var y := 100;
+ if * {
+ // we get here 0 times, because the compiler picks the other branch, which is empty
+ y := y + 2;
+ } // we get to the implicit else 1 time
+
+ if * {
+ // we get here 1 time
+ } else {
+ // we get here 0 times, because the compiler picks the other branch, which is empty
+ y := y + 2;
+ }
+
+ // the following if is all ghost, so there are no branch-coverage locations in it
+ if x < 2 {
+ } else if * {
+ }
+
+ if x < 2 {
+ // get here 0 times
+ } else if * {
+ // we get here 0 times
+ y := y + 1;
+ } // implicit else: 1 time
+}
+
+// ---------- if case ----------
+
+method Q(x: int) returns (y: int) {
+ // we get here 3 times
+
+ // the following statement is all ghost, so there are no coverage locations in it
+ if {
+ case x < 100 =>
+ case x < 1000 =>
+ assert x < 1_000_000;
+ case 50 <= x =>
+ }
+
+ if
+ case x < 100 =>
+ // we get here 1 time
+ case x < 1000 =>
+ // we get here 1 time, since the compiler lays down the cases in order
+ return 8;
+ case 50 <= x =>
+ // we get here 1 time
+}
+
+// ---------- while ----------
+
+method R(x: int) returns (y: int) {
+ // we get here 1 time
+ var i: nat := 0;
+ while i < x {
+ // we get here 111 times
+ i := i + 1;
+ }
+
+ while * {
+ // we get here 0 times
+ break;
+ }
+
+ while
+ decreases i
+ {
+ case i % 2 == 0 =>
+ // we get here 56 times
+ if i == 0 {
+ // we get here 1 time
+ break;
+ } // implicit else: 55 times
+ i := i - 1;
+ case i % 4 == 1 =>
+ // we get here 28 times
+ i := i - 1;
+ case 0 < i =>
+ // we get here 28 times
+ i := i - 1;
+ }
+
+ return 40;
+}
+
+// ---------- top-level if-then-else ----------
+
+function Fib(n: nat): nat {
+ // we get here 465 times
+ if n < 2 then // then: 233 times
+ n
+ else if false then // then: 0 times (else-if is omitted)
+ 8
+ else // else: 232 times
+ Fib(n - 2) + Fib(n - 1)
+}
+
+// ---------- top-level match expression, match statement, and tail recursion ----------
+
+function {:tailrecursion} Factorial(n: nat): nat {
+ // 11 times
+ match n
+ case 0 => 1 // 1 time
+ case _ => n * Factorial(n - 1) // 10 times
+}
+
+method {:tailrecursion} ComputeFactorial(n: nat, acc: nat) returns (f: nat)
+ ensures f == Factorial(n) * acc
+{
+ // 11 times
+ match n
+ case 0 => // 1 time
+ return acc;
+ case _ => // 10 times
+ f := ComputeFactorial(n - 1, acc * n);
+}
+
+// ---------- Main ----------
+
+method Main() {
+ // we get here 1 time
+
+ var mc := new MyClass();
+ mc := new MyClass();
+ mc := new MyClass();
+
+ var y := M(5);
+ y := M(y);
+ y := M(y);
+
+ y := N(5);
+ y := N(y);
+ y := N(y);
+
+ P(5);
+
+ y := Q(50);
+ y := Q(101);
+ y := Q(1010);
+
+ y := R(111);
+
+ y := Fib(12);
+
+ y := Factorial(10);
+ y := ComputeFactorial(10, 1);
+}
+
+
+
+
+
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
index dc530f4421e..eb76fc3925d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
@@ -1,10 +1,10 @@
// NONUNIFORM: Not a compiler test
// Verification coverage:
// RUN: rm -rf "%t"/coverage_verification
-// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --no-timestamp-for-coverage-report --coverage-report "%t/coverage_verification" %s
+// RUN: %baredafny verify --use-basename-for-filename --show-snippets false --verify-included-files --no-timestamp-for-coverage-report --verification-coverage-report "%t/coverage_verification" %s
// RUN: %sed 's/ "%t"/coverage_verification_actual.html
// RUN: %diff "%S/ProofDependencyLogging.dfy_verification.html.expect" "%t/coverage_verification_actual.html"
-// Test coverage:
+// Expected test coverage:
// RUN: rm -rf "%t"/coverage_testing
// RUN: %baredafny generate-tests Block --no-timestamp-for-coverage-report --coverage-report "%t/coverage_testing" %s
// RUN: %sed 's/ "%t"/coverage_testing_actual.html
diff --git a/docs/DafnyRef/Features.md b/docs/DafnyRef/Features.md
index f0b5c1a51ee..c09e18d0d67 100644
--- a/docs/DafnyRef/Features.md
+++ b/docs/DafnyRef/Features.md
@@ -44,7 +44,8 @@
| [Converting values to strings](#sec-print-statement) | X | X | X | X | X | | X |
| [Legacy CLI without commands](#sec-dafny-commands) | X | X | X | X | X | X | |
| [Separate compilation](#sec-compilation) | X | | X | X | X | X | X |
-| [All built-in types in runtime library](##sec-compilation-built-ins) | X | X | X | X | X | | X |
+| [All built-in types in runtime library](#sec-compilation-built-ins) | X | X | X | X | X | | X |
+| [Execution coverage report](#sec-dafny-test) | X | | | | | | |
[^compiler-feature-forall-note]: 'Sequentializing' a `forall` statement refers to compiling it directly to a series of nested loops
with the statement's body directly inside. The alternative, default compilation strategy
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index c4a85cfcd98..5b4d20ad5ed 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -479,6 +479,8 @@ In particular, it accepts the `--target` option that specifies the programming l
- `--output` - gives the folder and filename root for compilation artifacts
- `--methods-to-test` - the value is a (.NET) regular expression that is matched against the fully
qualified name of the method; only those methods that match are tested
+- `--coverage-report` - the value is a directory in which Dafny will save an html coverage report highlighting parts of
+ the program that execution of the tests covered.
The order in which the tests are run is not specified.
@@ -1512,12 +1514,13 @@ included in the proof.
These options can be specified in `dfyconfig.toml`, and this is typically the most convenient way to use them with the IDE.
More detailed information is available using either the `--log-format
-text` or `--coverage-report` option to `dafny verify`. The former will
+text` or `--verification-coverage-report` option to `dafny verify`. The former will
include a list of proof dependencies (including source location and
description) alongside every assertion batch in the generated log
whenever one of the two warning options above is also included. The
latter will produce a highlighted HTML version of your source code, in
-the same format used by `dafny generate-tests --coverage-report`,
+the same format used by `dafny test --coverage-report`
+and `dafny generate-tests --verification-coverage-report`,
indicating which parts of the program were used, not used, or partly
used in the verification of the entire program.
diff --git a/docs/dev/news/4625.feat b/docs/dev/news/4625.feat
index fc2354afce0..23ce498a469 100644
--- a/docs/dev/news/4625.feat
+++ b/docs/dev/news/4625.feat
@@ -1 +1 @@
-The new `--coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged.
+The new `--verification-coverage-report` flag to `dafny verify` creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for `dafny generate-tests --coverage-report` and files from the two commands can be merged.
diff --git a/docs/dev/news/4755.feat b/docs/dev/news/4755.feat
new file mode 100644
index 00000000000..5e5021687d5
--- /dev/null
+++ b/docs/dev/news/4755.feat
@@ -0,0 +1 @@
+The new `--coverage-report` flag to `dafny run` and `dafny test` creates an HTML report highlighting which portions of the program were executed at runtime.