Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow filtering of combined coverage reports #4673

Merged
merged 3 commits into from
Oct 17, 2023
Merged

Conversation

atomb
Copy link
Member

@atomb atomb commented Oct 16, 2023

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.

Description

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

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.
@atomb atomb requested a review from Dargones October 16, 2023 22:58
Comment on lines +94 to +96
if ((onlyLabel ?? span.Label) == span.Label) {
mergedReport.LabelCode(span.Span, span.Label);
}
Copy link
Collaborator

@Dargones Dargones Oct 16, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the intent here to display locations where both reports have the same label (i.e. intersection)? If yes, then there should be an else branch here that labels the code with the NotApplicable label. The report merged using the present approach will display the union between the two original reports.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not quite. The point is to highlight only the locations that, after merging (with union semantics), have the label specified on the command line. The expected output I've checked in looks the way I'd expect it to. The key use case I want to support is for NotCovered: highlight all locations that are not covered by either verification or tests.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Alternatively, you could see this code as taking the merged report and removing all highlighting that isn't in the specified category. The conditional is arguably a bit confusing, given that it both checks whether the option has been specified and whether the current label matches the requested label in one expression.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I see! So you can get the intersection if you don't use --only-label and the union if you do. This makes sense!

@Dargones Dargones self-requested a review October 17, 2023 16:34
@atomb atomb enabled auto-merge (squash) October 17, 2023 16:36
@atomb atomb merged commit cd70e30 into dafny-lang:master Oct 17, 2023
18 checks passed
@atomb atomb deleted the only-label branch January 4, 2024 16:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants