From a2730358cc66479d1e9936e08fc83dc1030fa7bd Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 16 Oct 2023 15:52:34 -0700 Subject: [PATCH 1/2] Allow filtering of combined coverage reports Add a new `--only-label` option to `merge-coverage-reports` to include only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option `--only-label NotCovered` will highlight only the regions not covered by either testing or verification. --- .../Commands/CoverageReportCommand.cs | 6 + Source/DafnyDriver/CoverageReporter.cs | 6 +- Test/logger/CoverageReport.dfy | 5 + ...cyLogging.dfy_combined_limited.html.expect | 484 ++++++++++++++++++ 4 files changed, 500 insertions(+), 1 deletion(-) create mode 100644 Test/logger/ProofDependencyLogging.dfy_combined_limited.html.expect diff --git a/Source/DafnyDriver/Commands/CoverageReportCommand.cs b/Source/DafnyDriver/Commands/CoverageReportCommand.cs index 846e71440b4..b5b538384c3 100644 --- a/Source/DafnyDriver/Commands/CoverageReportCommand.cs +++ b/Source/DafnyDriver/Commands/CoverageReportCommand.cs @@ -7,20 +7,26 @@ using System.IO; using System.Linq; using System.Threading.Tasks; +using DafnyCore; namespace Microsoft.Dafny; static class CoverageReportCommand { + public static readonly Option OnlyLabelOption = new("--only-label", + "Skip coverage labels other than the given one, after merging labels from the input reports."); + public static IEnumerable