From df2dbb8fbd63c135a6fb414b4fb38b1448b6ee6d Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 30 Sep 2022 14:08:47 -0500 Subject: [PATCH 1/3] Fix: Position of default argument to be at the call site, not definition This PR fixes #2801 --- Source/DafnyCore/AST/Expressions.cs | 6 +++-- .../Synchronization/DiagnosticsTest.cs | 26 ++++++++++++++++++- .../DafnyLanguageServer.csproj | 2 +- 3 files changed, 30 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/AST/Expressions.cs b/Source/DafnyCore/AST/Expressions.cs index b13d07d1da6..a68881b11f1 100644 --- a/Source/DafnyCore/AST/Expressions.cs +++ b/Source/DafnyCore/AST/Expressions.cs @@ -88,7 +88,7 @@ public virtual IEnumerable SubExpressions { get { yield break; } } - private RangeToken rangeToken; + private RangeToken rangeToken = null; // Contains tokens that did not make it in the AST but are part of the expression, // Enables ranges to be correct. @@ -96,7 +96,7 @@ public virtual IEnumerable SubExpressions { /// Creates a token on the entire range of the expression. /// Used only for error reporting. - public RangeToken RangeToken { + public virtual RangeToken RangeToken { get { if (rangeToken == null) { if (tok is RangeToken tokAsRange) { @@ -4087,6 +4087,8 @@ public DefaultValueExpression(IToken tok, Formal formal, TypeMap = typeMap; Type = Resolver.SubstType(formal.Type, typeMap); } + + public override RangeToken RangeToken => new RangeToken(tok, tok); } /// diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index 3c6738a46ce..ee871399824 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -13,6 +13,7 @@ using System.Linq; using System.Threading; using System.Threading.Tasks; +using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -162,6 +163,29 @@ decreases y await AssertNoDiagnosticsAreComing(CancellationToken); } + [TestMethod] + public async Task OpeningDocumentWithDefaultParamErrorHighlightsCallSite() { + var source = @" +function test(x: int := 99): bool + requires x >= 100 +{ + false +} + +method A() +{ + var b := test(); +} ".TrimStart(); + var documentItem = CreateTestDocument(source); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); + Assert.AreEqual(1, diagnostics.Length); + Assert.AreEqual(MessageSource.Verifier.ToString(), diagnostics[0].Source); + Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity); + Assert.AreEqual(diagnostics[0].Range.Start.Line, 8); + await AssertNoDiagnosticsAreComing(CancellationToken); + } + [TestMethod] public async Task OpeningDocumentWithVerificationErrorDoesNotReportDiagnosticsWithVerificationErrorsIfNotVerifyOnChange() { var source = @" @@ -898,7 +922,7 @@ await SetUp(new Dictionary() { private static void AssertDiagnosticListsAreEqualBesidesMigration(Diagnostic[] expected, Diagnostic[] actual) { Assert.AreEqual(expected.Length, actual.Length, $"expected: {expected.Stringify()}, but was: {actual.Stringify()}"); - foreach (var t in expected.Zip(actual)) { + foreach (var t in Enumerable.Zip(expected, actual)) { Assert.AreEqual(Relocator.OutdatedPrefix + t.First.Message, t.Second.Message, t.Second.ToString()); } } diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index aff9663132b..706b9548af9 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -3,7 +3,7 @@ Exe net6.0 - false + true enable Microsoft.Dafny.LanguageServer ..\..\Binaries\ From ac0785194f2662d4e1202d4ff4819b29e3a2cd91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Tue, 4 Oct 2022 13:56:00 -0500 Subject: [PATCH 2/3] Update RELEASE_NOTES.md --- RELEASE_NOTES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 5835ba9ce75..3e915f5926a 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,5 +1,7 @@ # Upcoming +- fix: Correct error highlighting on function called with default arguments (https://github.com/dafny-lang/dafny/pull/2826) + # 3.9.0 - feat: Support for testing certain contracts at runtime with a new `/testContracts` flag (https://github.com/dafny-lang/dafny/pull/2712) From 204a99ce42352767b3cf5069176c3b6c69f415e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Wed, 12 Oct 2022 10:20:08 -0500 Subject: [PATCH 3/3] Create 2826.fix --- docs/dev/news/2826.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/2826.fix diff --git a/docs/dev/news/2826.fix b/docs/dev/news/2826.fix new file mode 100644 index 00000000000..d9d83c0a4e9 --- /dev/null +++ b/docs/dev/news/2826.fix @@ -0,0 +1 @@ +Correct error highlighting on function called with default arguments