Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Prevent incorrect internal error message #5320

Merged
merged 12 commits into from
Apr 16, 2024
Merged

Prevent incorrect internal error message #5320

merged 12 commits into from
Apr 16, 2024

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Apr 15, 2024 •
edited
Loading

Fixes #5209
Fixes #5295

Description

  • When mentioning an internal error due to verification timing out, throw an exception, so no successful verification message is emitted.
  • Wait longer before concluding the Boogie back-end is ignoring the verification timeout.
  • Update MultiBackendTest so it allows overriding default options.

How has this been tested?

Manually made code edits to simulate Boogie not returning, resulting in:

Exit code is 134 (Unhandled exception. System.Exception: Dafny encountered an internal error while waiting for C._ctor to verify.
   at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+MoveNext() in /Users/rwillems/SourceCode/dafny/Source/DafnyDriver/CliCompilation.cs:line 253
   at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+System.Threading.Tasks.Sources.IValueTaskSource<System.Boolean>.GetResult()
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 50

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) April 15, 2024 12:02
atomb
atomb reviewed Apr 15, 2024
View reviewed changes
Source/DafnyDriver/CliCompilation.cs Outdated
@@ -22,15 +22,18 @@ namespace DafnyDriver.Commands;
public record CanVerifyResult(ICanVerify CanVerify, IReadOnlyList<VerificationTaskResult> Results);

public class CliCompilation {
private readonly ILogger<CliCompilation> logger;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks like it's never used. Am I missing something?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unused indeed. Usage only occurred in a previous commit. Removed it.

atomb
atomb approved these changes Apr 16, 2024
View reviewed changes
Copy link
Member

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

@keyboardDrummer keyboardDrummer merged commit 67db058 into dafny-lang:master Apr 16, 2024
20 checks passed
@keyboardDrummer keyboardDrummer deleted the preventIncorrectInternalErrorMessage branch April 17, 2024 08:53
@keyboardDrummer keyboardDrummer mentioned this pull request Apr 29, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@atomb atomb atomb approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Error: Dafny encountered an internal error while waiting for this symbol to verify. internal error
2 participants
@keyboardDrummer @atomb