Verification coverage report #4625
Conversation
Also move some code around.
Source/DafnyTestGeneration/Main.cs
Outdated
| var source = new StreamReader(program.GetStartOfFirstFileToken().ActualFilename).ReadToEnd(); | ||
| var lines = source.Split("\n"); | ||
| var pos = 0; | ||
| var line = 0; | ||
| var linePositions = new int[lines.Length]; | ||
| while (pos < source.Length) { | ||
| linePositions[line] = pos; | ||
| pos += lines[line].Length + 1; | ||
| line++; | ||
| } |
There was a problem hiding this comment.
A test coverage report might include several files, but the linePositions array only works if there is only one file. I think something like this should work.
There was a problem hiding this comment.
Ah, of course. I was mistakenly carrying over my mental model from another location that was file-specific. Thanks for fixing it!
| for (var pos = span.Span.StartToken.pos; pos <= span.Span.EndToken.pos; pos++) { | ||
| characterLabels[pos] = CoverageLabelExtension.Combine(characterLabels[pos], span.Label); | ||
| } |
There was a problem hiding this comment.
Have just realized that this loop replaces about 30 lines of some binary search recursion madness I wrote...
There was a problem hiding this comment.
I originally started thinking about interval trees when I realized that I needed to deal with arbitrary types and degrees of overlap. And then I realized that just tracking the labels on a per-character basis was simpler and probably even more efficient.
| @@ -239,16 +265,30 @@ public class CoverageReporter { | |||
| private string HtmlReportForFile(CoverageReport report, string pathToSourceFile, string baseDirectory, string linksToOtherReports) { | |||
| var source = new StreamReader(pathToSourceFile).ReadToEnd(); | |||
| var lines = source.Split("\n"); | |||
| IToken lastToken = new Token(0, 0); | |||
| var characterLabels = new CoverageLabel[source.Length]; | |||
There was a problem hiding this comment.
Is it worth explicitly initializing values with None so that the order of labels in the CoverageLabel enum doesn't affect the behavior?
There was a problem hiding this comment.
Yeah, good catch. I'll change that.
Fix line number to pos conversion
Avoids the fragility of depending on the declaration order in the enum.
# Description Adds support for producing reports describing verification coverage in the same format used for the expected test coverage reports that can be produced from `dafny generate-tests`. Verification and test coverage reports can be merged using `dafny merge-coverage-reports`. # How has this been tested? Includes a test of expected output in `Test/logger/ProofDependencyLogging.dfy_verification.html.expect`. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]>
Description
Adds support for producing reports describing verification coverage in the same format used for the expected test coverage reports that can be produced from
dafny generate-tests. Verification and test coverage reports can be merged usingdafny merge-coverage-reports.How has this been tested?
Includes a test of expected output in
Test/logger/ProofDependencyLogging.dfy_verification.html.expect.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.