Disgard previous notifications to ensure we get only the most recent …

…ones. One test for possible interleavings.
dafny-lang · Mar 29, 2022 · beabc4f · beabc4f
1 parent 0a2ff43
commit beabc4f
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 3 deletions.
diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs b/Source/DafnyLanguageServer.Test/Diagnostics/LinearVerificationDiagnosticTester.cs
@@ -118,6 +118,9 @@ var previousPerLineDiagnostics
  for (; maximumNumberOfTraces > 0; maximumNumberOfTraces--) {
  var verificationDiagnosticReport = await VerificationDiagnosticReceiver.AwaitNextNotificationAsync(CancellationToken);
  Assert.AreEqual(documentItem.Uri, verificationDiagnosticReport.Uri);
+ if (documentItem.Version != verificationDiagnosticReport.Version) {
+ continue;
+ }
  var newPerLineDiagnostics = verificationDiagnosticReport.PerLineDiagnostic.ToList();
  if ((previousPerLineDiagnostics != null
  && previousPerLineDiagnostics.SequenceEqual(newPerLineDiagnostics)) ||
@@ -229,7 +232,9 @@ public async Task VerifyTrace(string codeAndTrace) {
  }
  var traceObtained = RenderTrace(traces, code);
  var ignoreQuestionMarks = AcceptQuestionMarks(traceObtained, codeAndTrace);
- AssertWithDiff.Equal("\n" + codeAndTrace + "\n", "\n" + ignoreQuestionMarks + "\n");
+ var expected = "\n" + codeAndTrace + "\n";
+ var actual = "\n" + ignoreQuestionMarks + "\n";
+ AssertWithDiff.Equal(expected, actual);
  }
 
  // Finds all the "?" at the beginning in expected and replace the characters at the same position in traceObtained

diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/SimpleLinearVerificationDiagnosticTester.cs b/Source/DafnyLanguageServer.Test/Diagnostics/SimpleLinearVerificationDiagnosticTester.cs
@@ -68,15 +68,17 @@ await VerifyTrace(@"
  . S [S][ ]:}");
  }
 
- [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ [TestMethod, Timeout(MaxTestExecutionTimeMs * 10)]
  public async Task EnsureNoAssertShowsVerified() {
- await VerifyTrace(@"
+ for (var i = 0; i < 10; i++) {
+ await VerifyTrace(@"
  . | | | I | :predicate P(x: int)
  | | | I | :
  . S [S][ ][I] | :method Main() {
  . S [=][=][I] | : ghost var x :| P(x); //Next: ghost var x := 1;
  . S [S][ ][I] | :}
  | :");
+ }
  }
 
  [TestMethod, Timeout(MaxTestExecutionTimeMs)]