Skip to content

Commit

Permalink
Make DiagnosticsForVerificationTimeoutHasNameAsRange stable (dafny-la…
Browse files Browse the repository at this point in the history
…ng#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

<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 authored Sep 10, 2023
1 parent ed13e3c commit c54bd2d
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down

0 comments on commit c54bd2d

Please sign in to comment.