Test for unsupported feature too

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -3443,7 +3443,7 @@ protected class ClassWriter : IClassWriter {
  TrStmt(recoveryBody, catchBlock);
  }
 
- protected override void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {
+ protected void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {
  wr.WriteLine(@"
 namespace DafnyProfiling {
  public class CodeCoverage {

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -56,7 +56,8 @@ class CppCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.UnicodeChars,
  Feature.ConvertingValuesToStrings,
- Feature.BuiltinsInRuntime
+ Feature.BuiltinsInRuntime,
+ Feature.RuntimeCoverageReport
  };
 
  private List<DatatypeDecl> datatypeDecls = new();

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -91,7 +91,8 @@ class DafnyCompiler : SinglePassCompiler {
  Feature.SubtypeConstraintsInQuantifiers,
  Feature.TuplesWiderThan20,
  Feature.ForLoops,
- Feature.Traits
+ Feature.Traits,
+ Feature.RuntimeCoverageReport
  };
 
  private readonly List<string> Imports = new() { DafnyDefaultModule };

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -27,7 +27,8 @@ class GoCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.ExternalConstructors,
  Feature.SubsetTypeTests,
- Feature.AllUnderscoreExternalModuleNames
+ Feature.AllUnderscoreExternalModuleNames,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -29,7 +29,9 @@ public class JavaCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.TuplesWiderThan20,
  Feature.ArraysWithMoreThan16Dims,
- Feature.ArrowsWithMoreThan16Arguments
+ Feature.ArrowsWithMoreThan16Arguments,
+ Feature.RuntimeCoverageReport,
+ Feature.RuntimeCoverageReport
  };
 
  const string DafnySetClass = "dafny.DafnySet";

Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs

@@ -26,7 +26,8 @@ class JavaScriptCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.ExternalConstructors,
  Feature.SubsetTypeTests,
- Feature.SeparateCompilation
+ Feature.SeparateCompilation,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -34,7 +34,8 @@ class PythonCompiler : SinglePassCompiler {
 
  public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
  Feature.SubsetTypeTests,
- Feature.MethodSynthesis
+ Feature.MethodSynthesis,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -6061,9 +6061,5 @@ private class ArrayLvalueImpl : ILvalue {
  }
 
  protected abstract void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr);
-
- protected virtual void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {
- throw new UnsupportedFeatureException(program.GetStartOfFirstFileToken(), Feature.RuntimeCoverageReport);
- }
  }
 }

Source/DafnyCore/Feature.cs

@@ -186,7 +186,7 @@ public enum Feature {
  [FeatureDescription("All built-in types in runtime library", "#sec-compilation-built-ins")]
  BuiltinsInRuntime,
 
- [FeatureDescription("Runtime coverage report", "#sec-compilation-built-ins")]
+ [FeatureDescription("Execution coverage report", "#sec-compilation-built-ins")]
  RuntimeCoverageReport
 }
 

Source/DafnyDriver/CompilerDriver.cs

@@ -492,6 +492,11 @@ private record TargetPaths(string Directory, string Filename) {
  foreach (var compilerInstrumenter in options.Plugins.SelectMany(p => p.GetCompilerInstrumenters(dafnyProgram.Reporter))) {
  options.Backend.InstrumentCompiler(compilerInstrumenter, dafnyProgram);
  }
+
+ if (options.Get(CommonOptionBag.ExecutionCoverageReport) != null 
+ && options.Backend.UnsupportedFeatures.Contains(Feature.RuntimeCoverageReport)) {
+ throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.RuntimeCoverageReport);
+ }
 
  var compiler = options.Backend;
 
@@ -565,7 +570,7 @@ private record TargetPaths(string Directory, string Filename) {
  var coverageReportDir = options.Get(CommonOptionBag.ExecutionCoverageReport);
  if (coverageReportDir != null) {
  var coverage = compiler.GetCoverageAfterRun();
- var coverageReport = new CoverageReport("Test Coverage", "Branches", "_tests_actual", dafnyProgram);
+ var coverageReport = new CoverageReport("Execution Coverage", "Branches", "_tests_actual", dafnyProgram);
  coverage.PopulateCoverageReport(coverageReport);
  new CoverageReporter(options).SerializeCoverageReports(coverageReport, coverageReportDir);
  }

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy

@@ -4,8 +4,17 @@
 // (See also logger/CoverageReport.dfy for verification coverage and expected coverage of generated tests)
 
 // RUN: rm -rf "%t"/execution_testing
-// RUN: %baredafny run %args -t:cs --no-timestamp-for-coverage-report --coverage-report "%t/execution_testing" %s
-// RUN: %sed 's/<h1 hidden.*//' "%t"/execution_testing/BranchCoverage.dfy_tests_actual.html > "%t"/coverage_tests_actual.html
-// RUN: %diff "%S/CoverageReport.dfy_tests_actual.html.expect" "%t/coverage_tests_actual.html"
+// RUN: %baredafny run %args -t:cs --no-timestamp-for-coverage-report --coverage-report "%t_coverage_reports/execution_testing" %s
+// RUN: %sed 's/<h1 hidden.*//' "%t_coverage_reports"/execution_testing/BranchCoverage.dfy_tests_actual.html > "%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"

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

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CoverageReport.dfy_tests_actual.html.expect

@@ -5,14 +5,14 @@
 <head>
  <meta http-equiv="Content-Type" content="text/html;charset=UTF-8"/>
  <link rel="stylesheet" href="./.resources/coverage.css" type="text/css"/>
- <title>BranchCoverage.dfy, Test Coverage</title>
+ <title>BranchCoverage.dfy, Execution Coverage</title>
 </head>
 <body onload="window['PR_TAB_WIDTH']=4">
 <div class="menu" id="menu">
  <a href="./index_tests_actual.html">Index</a>
 
 </div>
-<h1>BranchCoverage.dfy, Test Coverage</h1>
+<h1>BranchCoverage.dfy, Execution Coverage</h1>
 
 <pre class="source lang-java linenums">
 <span class="na" id="1:1">// RUN: %dafny /useBaseNameForFileName /compile:3 /coverage:- /spillTargetCode:1 /compileTarget:cs %S/BranchCoverage2.cs "%s" > "%t"