Rename --coverage-report to --expected-coverage-report (#5301)

### Description Rename --coverage-report to --expected-coverage-report ### How has this been tested? Updated CLI test <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang · Apr 9, 2024 · a2004d2 · a2004d2
1 parent b292647
commit a2004d2
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 6 deletions.
diff --git a/Source/DafnyDriver/Commands/DeadCodeCommand.cs b/Source/DafnyDriver/Commands/DeadCodeCommand.cs
@@ -15,7 +15,7 @@ static class DeadCodeCommand {
  new Option[] {
  GenerateTestsCommand.LoopUnroll,
  GenerateTestsCommand.SequenceLengthLimit,
- GenerateTestsCommand.CoverageReport,
+ GenerateTestsCommand.ExpectedCoverageReport,
  GenerateTestsCommand.ForcePrune,
  GenerateTestsCommand.PrintBpl,
  BoogieOptionBag.SolverLog,

diff --git a/Source/DafnyDriver/Commands/GenerateTestsCommand.cs b/Source/DafnyDriver/Commands/GenerateTestsCommand.cs
@@ -28,7 +28,7 @@ static class GenerateTestsCommand {
  BoogieOptionBag.SolverResourceLimit,
  BoogieOptionBag.VerificationTimeLimit,
  PrintBpl,
- CoverageReport,
+ ExpectedCoverageReport,
  CommonOptionBag.NoTimeStampForCoverageReport,
  ForcePrune,
  }.Concat(DafnyCommands.ConsoleOutputOptions.Except(new[] { CommonOptionBag.AllowWarnings }).ToList()).
@@ -133,7 +133,7 @@ private enum Mode {
  "Print the Boogie code used during test generation.") {
  ArgumentHelpName = "filename"
  };
- public static readonly Option<string> CoverageReport = new("--coverage-report",
+ public static readonly Option<string> ExpectedCoverageReport = new(new[] { "--expected-coverage-report", "--coverage-report" },
  "Emit expected test coverage report to a given directory.") {
  ArgumentHelpName = "directory"
  };
@@ -149,7 +149,7 @@ private enum Mode {
  DafnyOptions.RegisterLegacyBinding(PrintBpl, (options, value) => {
  options.TestGenOptions.PrintBpl = value;
  });
- DafnyOptions.RegisterLegacyBinding(CoverageReport, (options, value) => {
+ DafnyOptions.RegisterLegacyBinding(ExpectedCoverageReport, (options, value) => {
  options.TestGenOptions.CoverageReport = value;
  });
  DafnyOptions.RegisterLegacyBinding(ForcePrune, (options, value) => {
@@ -160,7 +160,7 @@ private enum Mode {
  LoopUnroll,
  SequenceLengthLimit,
  PrintBpl,
- CoverageReport,
+ ExpectedCoverageReport,
  ForcePrune
  );
  }

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/CoverageReport.dfy
@@ -6,7 +6,7 @@
 // RUN: %diff "%S/ProofDependencies.dfy_verification.html.expect" "%t/coverage_verification_actual.html"
 // 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: %baredafny generate-tests Block --no-timestamp-for-coverage-report --expected-coverage-report "%t/coverage_testing" %s
 // RUN: %sed 's/<h1 hidden.*//' "%t"/coverage_testing/ProofDependencies.dfy_tests_expected.html > "%t"/coverage_testing_actual.html
 // RUN: %diff "%S/ProofDependencies.dfy_tests_expected.html.expect" "%t/coverage_testing_actual.html"
 // Combined coverage:

diff --git a/docs/dev/news/5301.fix b/docs/dev/news/5301.fix
@@ -0,0 +1 @@
+Rename the `dafny generate-tests` option `--coverage-report` to `--expected-coverage-report`