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/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