search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.87k stars 256 forks source link

Unstable BetterMessageWhenOneAssertPerBatch test #2720

Open keyboardDrummer opened 2 years ago

keyboardDrummer commented 2 years ago 
Starting test execution, please wait...
A total of 1 test files matched the specified pattern.
  Failed BetterMessageWhenOneAssertPerBatch [471 ms]
  Error Message:
   Assert.IsTrue failed. [**Error:**](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-debugging) assertion might not hold  
This is the only assertion in [batch](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-attributes-on-assert-statements) #2 of 2 in method f  
[Batch](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-attributes-on-assert-statements) #2 resource usage: 8K RU did not match \[\*\*Error:\*\*]\(.*\)\ assertion\ might\ not\ hold\ \ \nThis\ is\ the\ only\ assertion\ in\ \[batch]\(.*\)\ \#2\ of\ 3\ in\ method\ f\ \ \n\[Batch]\(.*\)\ \#2\ resource\ usage:\ .*\ RU.
The result string did not contain ') #2 of 3 in method f  
[Batch]('
  Stack Trace:
     at Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup.HoverVerificationTest.AssertMatchRegex(String expected, String value) in D:\a\dafny\dafny\Source\DafnyLanguageServer.Test\Lookup\HoverVerificationTest.cs:line 264
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup.HoverVerificationTest.AssertHoverMatches(TextDocumentItem documentItem, Position hoverPosition, String expected) in D:\a\dafny\dafny\Source\DafnyLanguageServer.Test\Lookup\HoverVerificationTest.cs:line 250
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup.HoverVerificationTest.BetterMessageWhenOneAssertPerBatch() in D:\a\dafny\dafny\Source\DafnyLanguageServer.Test\Lookup\HoverVerificationTest.cs:line 91

  Standard Output Messages:
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       MarkVerificationFinished called
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown top level declaration string of type Microsoft.Dafny.TypeSynonymDecl
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown top level declaration nat of type Microsoft.Dafny.SubsetTypeDecl
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown syntax node of type Microsoft.Dafny.FunctionCallExpr in (null)@(0,0)
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown syntax node of type Microsoft.Dafny.FunctionCallExpr in (null)@(0,0)
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown top level declaration _#PartialFunc1 of type Microsoft.Dafny.SubsetTypeDecl
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown top level declaration _#TotalFunc1 of type Microsoft.Dafny.SubsetTypeDecl
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown syntax node of type Microsoft.Dafny.FunctionCallExpr in (null)@(0,0)
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown syntax node of type Microsoft.Dafny.FunctionCallExpr in (null)@(0,0)
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown top level declaration _#PartialFunc0 of type Microsoft.Dafny.SubsetTypeDecl
 dbug: Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver[0]
       encountered unknown top level declaration _#TotalFunc0 of type Microsoft.Dafny.SubsetTypeDecl
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       documentUpdates.HasObservers: True, threadId: 1129
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       IdeStateObserver.OnNext entered, threadId: 1129
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       Publishing notification for file:///testfile.dfy version 1.
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       Passed documentAfterParsing to documentUpdates.OnNext, resolving ResolvedDocument task for version 1.
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       IdeStateObserver.OnNext entered, threadId: 1129
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       Publishing notification for file:///testfile.dfy version 1.
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       MarkVerificationStarted called
 info: Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier[0]
 info: Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier[0]
       Verifying f (correctness) ...
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       Received status Running { } for Impl$$_module.__default.f
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       IdeStateObserver.OnNext entered, threadId: 1182
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       Publishing notification for file:///testfile.dfy version 1.
 dbug: Microsoft.Dafny.LanguageServer.Workspace.DocumentManager[0]
       Setting result for workCompletedForCurrentVersion
 dbug: Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler[0]
       received hover request for file:///testfile.dfy
 dbug: Microsoft.Dafny.LanguageServer.Workspace.DocumentManager[0]
       GetSnapshotAfterResolutionAsync, resolvedDocument.Version = 1, observer.LastPublishedState.Version = 1, threadId: 1129
 dbug: Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler[0]
       no symbol was found at (line: 0, char: 0) in file:///testfile.dfy
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       LastDocument will return document version 1
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       Received status Completed { Result = Microsoft.Boogie.VerificationResult } for Impl$$_module.__default.f
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       IdeStateObserver.OnNext entered, threadId: 1182
 dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
       Publishing notification for file:///testfile.dfy version 1.
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       Calling FinishedNotifications because there are no remaining verification jobs for version 1.
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       MarkVerificationFinished called
 dbug: Microsoft.Dafny.LanguageServer.Workspace.Compilation[0]
       verificationCompleted finished with status RanToCompletion
 dbug: Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler[0]
       received hover request for file:///testfile.dfy
 dbug: Microsoft.Dafny.LanguageServer.Workspace.DocumentManager[0]
       GetSnapshotAfterResolutionAsync, resolvedDocument.Version = 1, observer.LastPublishedState.Version = 1, threadId: 1174
 dbug: Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler[0]
       no symbol was found at (line: 1, char: 12) in file:///testfile.dfy
MikaelMayer commented 2 years ago

Hum. Hovering will display all available information. So if two assertion batches have completed, it will display them. However, these tests normally explicitly wait for the verification to finish, meaning there should be no more assertion batches when it triggers the hover and checks the hover message. Do you know if there is a way the test could start before the last assertion batch is added?

keyboardDrummer commented 2 years ago

It says there were only 2 instead of 3 total assertions, so it seems to be a preprocessing problem instead of a waiting one, don't you think?