Feature request: runtime branch coverage #4671
Assignees
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Milestone
Comments
robin-aws
added a commit
that referenced
this issue
Nov 9, 2023
### Description Implements an execution coverage report in the same format as the existing verification coverage and expected generated test coverage reports. Mainly this just meant using the existing low-level instrumentation provided by the old CLI `/coverage` option to write coverage data to a temporary file during execution, and then parsing this data and populating a `CoverageReport` object. I've only implemented this for C# for now, since the execution coverage SHOULD generally be identical across languages (the instrumentation is emitted from the common SinglePassCompiler) but it wouldn't take much work to hook it up for the other backends. Also adds this to the `DafnyStandardLibraries` project, and augments the existing coverage report generation to handle `.doo` files and Uris somewhat better. Also renames the existing verification option `--coverage-report` to `--verification-coverage-report`, since this option is almost always in scope (since most commands run verification), and for `dafny test` and `dafny run` "coverage report" more naturally means execution coverage instead. The former hasn't been released yet so this won't break anyone. :) Resolves #4671 ### How has this been tested? `comp/CoverageReport.dfy`, similar to the existing `logger/CoverageReport.dfy`
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This is partially implemented already, as we have a
/coverageoption implemented for most backends: https://github.com/dafny-lang/dafny/blob/master/Test/comp/BranchCoverage.dfy.This option is really more of a branch coverage plugin interface, though: users have to provide their own coverage event callback handler, such as https://github.com/dafny-lang/dafny/blob/master/Test/comp/BranchCoverage2.cs. The feature that users will actually want is a simple switch to emit a coverage report, and the ability to set a minimum threshold for the coverage percentage.
I suggest providing a
--coverage-reportoption fordafny runanddafny test, just as we already have fordafny generate-tests(which shows the expected runtime coverage). Since the runtime coverage emitted by every backend should be the same, we'll get a lot of benefit from just supporting the C# backend for now. We can hook up the existing/coverageinstrumentation to the existingCoverageReportC# class.The text was updated successfully, but these errors were encountered: