Skip to content

Commit

Permalink
Documenting Test Generation in Reference Manual (#4445)
Browse files Browse the repository at this point in the history
This pull request documents the `generate-tests` command. 

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]>
Co-authored-by: Aaron Tomb <[email protected]>
  • Loading branch information
3 people authored Aug 27, 2023
1 parent 95eb74b commit 528b593
Show file tree
Hide file tree
Showing 4 changed files with 188 additions and 161 deletions.
13 changes: 3 additions & 10 deletions Source/DafnyTestGeneration/Main.cs
Original file line number Diff line number Diff line change
Expand Up @@ -27,13 +27,11 @@ public static async IAsyncEnumerable<string> GetDeadCodeStatistics(Program progr

program.Reporter.Options.PrintMode = PrintModes.Everything;

var blocksReached = 0;
HashSet<string> allStates = new();
HashSet<string> allDeadStates = new();

// Generate tests based on counterexamples produced from modifications
foreach (var modification in GetModifications(cache, program, out _)) {
blocksReached++;
await modification.GetCounterExampleLog(cache);
var deadStates = new HashSet<string>();
if (!modification.IsCovered(cache)) {
Expand All @@ -44,23 +42,18 @@ public static async IAsyncEnumerable<string> GetDeadCodeStatistics(Program progr
foreach (var capturedState in deadStates) {
yield return $"Code at {capturedState} is potentially unreachable.";
}
blocksReached--;
allDeadStates.UnionWith(deadStates);
}

foreach (var state in modification.CapturedStates) {
if (!allStates.Contains(state)) {
if (deadStates.Count == 0 && !allStates.Contains(state)) {
yield return $"Code at {state} is reachable.";
allStates.Add(state);
}
allStates.Add(state);
}
}

yield return $"Out of {blocksReached} basic blocks " +
$"({allStates.Count} capturedStates), {blocksReached} " +
$"({allStates.Count - allDeadStates.Count}) are reachable. " +
"There might be false negatives if you are not unrolling " +
"loops. False positives are always possible.";
yield return $"Out of {allStates.Count} basic blocks, {allStates.Count - allDeadStates.Count} are reachable.";
}

public static async IAsyncEnumerable<string> GetDeadCodeStatistics(TextReader source, Uri uri, DafnyOptions options, CoverageReport report = null) {
Expand Down
141 changes: 0 additions & 141 deletions Source/DafnyTestGeneration/README.md

This file was deleted.

Loading

0 comments on commit 528b593

Please sign in to comment.