Skip to content

Commit

Permalink
Timeout reporting (#5393)
Browse files Browse the repository at this point in the history
### Description
- Fix bug in reporting of time taken when a verification timeout occurs
- Make test 3855 stable by redacting the time taken

### How has this been tested?
- Fix is not tested
- Flaky test is updated

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer committed May 2, 2024
1 parent 79c323d commit 075b2a8
Show file tree
Hide file tree
Showing 3 changed files with 11 additions and 10 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyDriver/Commands/VerifyCommand.cs
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ public static class VerifyCommand {
var batchReporter = new BatchErrorReporter(compilation.Options);
foreach (var completed in result.Results) {
Compilation.ReportDiagnosticsInResult(compilation.Options, result.CanVerify.FullDafnyName, completed.Task.Token,
(uint)completed.Result.RunTime.Seconds,
(uint)completed.Result.RunTime.TotalSeconds,
completed.Result, batchReporter);
}
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
// RUN: %exits-with 4 %baredafny verify --show-snippets:false --allow-axioms --allow-deprecation --use-basename-for-filename "%s" > "%t"
// RUN: %exits-with 4 %baredafny verify --show-snippets:false --allow-axioms --allow-deprecation --use-basename-for-filename "%s" > "%t".raw
// RUN: %sed 's/after \d+ seconds/after <redacted> seconds/' %t.raw > "%t"
// RUN: %diff "%s.expect" "%t"
// Nearly verbatim copy of the text case given in the issue
//SIMULADA
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
git-issue-3855.dfy(800,0): Warning: attribute :ignore is deprecated
git-issue-3855.dfy(800,11): Error: Verification of 'Memory.dynMove' timed out after 1 seconds
git-issue-3855.dfy(943,17): Error: a precondition for this call could not be proved
git-issue-3855.dfy(429,29): Related location: this is the precondition that could not be proved
git-issue-3855.dfy(943,17): Error: a precondition for this call could not be proved
git-issue-3855.dfy(433,36): Related location: this is the precondition that could not be proved
git-issue-3855.dfy(1336,20): Error: a precondition for this call could not be proved
git-issue-3855.dfy(433,36): Related location: this is the precondition that could not be proved
git-issue-3855.dfy(801,0): Warning: attribute :ignore is deprecated
git-issue-3855.dfy(801,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds
git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved
git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved
git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved
git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved
git-issue-3855.dfy(1337,20): Error: a precondition for this call could not be proved
git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved

Dafny program verifier finished with 101 verified, 3 errors, 1 time out

0 comments on commit 075b2a8

Please sign in to comment.