Skip to content

Commit

Permalink
Allow text and csv loggers together (dafny-lang#4714)
Browse files Browse the repository at this point in the history
An extraneous `return` was preventing multiple verification loggers from
running.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.
  • Loading branch information
atomb authored Oct 25, 2023
1 parent 7312fc7 commit c63eeca
Show file tree
Hide file tree
Showing 2 changed files with 42 additions and 1 deletion.
1 change: 0 additions & 1 deletion Source/DafnyDriver/VerificationResultLogger.cs
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,6 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa
var textLogger = new TextLogger(depManager, options.OutputWriter);
textLogger.Initialize(parameters);
textLogger.LogResults(verificationResults);
return;
} else {
throw new ArgumentException($"unsupported verification logger config: {loggerConfig}");
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
// RUN: %exits-with 4 %baredafny verify --log-format:text --log-format:csv";"LogFileName="%t.csv" "%s" > "%t"
// RUN: %OutputCheck --file-to-check "%t" "%s"
// CHECK: Overall outcome: Errors
// Check that the CSV file exists
// RUN: %diff "%t.csv" "%t.csv"

method ExampleWithSplits() returns (y: int)
ensures y >= 0
{
var x: int;
x := 5;
y := 0;
while (x > 0)
invariant x + y == 5
invariant x*x <= 25
{
x := x - 1;
assert {:split_here} (x+y) * (x+y) > 25;
y := y + 1;
if (x < 3) {
assert 2 < 2;
assert {:split_here} y*y > 4;
}
else {
assert {:split_here} y*y*y < 8;
assert 2 < 2;
}
assert {:split_here} (x+y) * (x+y) == 25;
}
}

method ExampleWithoutSplits() {
assert 1 + 1 == 2;
assert 2 + 2 == 4;
assert 3 + 3 == 6;
}

method AnotherExampleWithoutSplits() {
assert 1 + 1 == 2;
assert 2 + 2 == 4;
assert 3 + 3 == 6;
}

0 comments on commit c63eeca

Please sign in to comment.