From c54bd2db2270d211b9eb97435667eb411bd66d6a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sun, 10 Sep 2023 10:59:25 +0200 Subject: [PATCH] Make DiagnosticsForVerificationTimeoutHasNameAsRange stable (#4528) ### Changes Prevent unit test failures by not relying on an absolute time limit but a resource limit instead. ### Testing Changes are to a test 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). --- .../DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs | 2 +- .../Synchronization/DiagnosticsTest.cs | 4 ++-- .../Synchronization/VerificationStatusTest.cs | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index 10f96cb01ae..e4950514827 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -26,7 +26,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest { public class DafnyLanguageServerTestBase : LanguageProtocolTestBase { protected readonly string SlowToVerify = @" -lemma {:timeLimit 1} SquareRoot2NotRational(p: nat, q: nat) +lemma {:rlimit 100} SquareRoot2NotRational(p: nat, q: nat) requires p > 0 && q > 0 ensures (p * p) != 2 * (q * q) { diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index 4297154ce18..80f92dfdbe4 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -90,8 +90,8 @@ public async Task DiagnosticsForVerificationTimeoutHasNameAsRange() { var documentItem = CreateTestDocument(SlowToVerify, "DiagnosticsForVerificationTimeout.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); - Assert.Contains("timed out", diagnostics[0].Message); - Assert.Equal(new Range(0, 21, 0, 43), diagnostics[0].Range); + Assert.Contains("Verification out of resource", diagnostics[0].Message); + Assert.Equal(new Range(0, 20, 0, 42), diagnostics[0].Range); } [Fact] diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 37aab2cfce0..1400b2f3a47 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -367,7 +367,7 @@ await SetUp(options => { var successfulRun = await client.RunSymbolVerification(new TextDocumentIdentifier(documentItem.Uri), methodHeader, CancellationToken); Assert.True(successfulRun); - var range = new Range(0, 21, 0, 43); + var range = new Range(0, 20, 0, 42); await WaitForStatus(range, PublishedVerificationStatus.Running, CancellationToken); await WaitForStatus(range, PublishedVerificationStatus.Error, CancellationToken);