fix: "Failing precondition" on tooltip instead of "return path"

RELEASE_NOTES.md

@@ -3,7 +3,7 @@
 - feat: Support for the `{:opaque}` attibute on `const` (https://github.com/dafny-lang/dafny/pull/2545)
 - feat: Support for plugin-based code actions on the IDE (https://github.com/dafny-lang/dafny/pull/2021)
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
-
+- fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654)
 
 # 3.8.0
 

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -99,7 +99,7 @@ This is the only assertion in [batch](???) #2 of 3 in method f
       await AssertHoverMatches(documentItem, (2, 12),
         @"<span style='color:green'>**Success:**</span> assertion always holds  
 This is the only assertion in [batch](???) #3 of 3 in method f  
-[Batch](???) #3 resource usage: ??? RU  "
+[Batch](???) #3 resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (0, 36),
         @"**Verification performance metrics for method f**:
@@ -132,7 +132,7 @@ await AssertHoverMatches(documentItem, (2, 12),
       await AssertHoverMatches(documentItem, (3, 26),
         @"[**Error:**](???) assertion might not hold  
 This is assertion #1 of 2 in [batch](???) #2 of 2 in function f  
-[Batch](???) #2 resource usage: ??? RU  "
+[Batch](???) #2 resource usage: ??? RU"
       );
       await AssertHoverMatches(documentItem, (0, 36),
         @"**Verification performance metrics for function f**:
@@ -150,7 +150,6 @@ public async Task MeaningfulMessageWhenMethodWithoutAssert() {
 method f(x: int) {
   print x;
 }", "testfile.dfy", CompilationStatus.VerificationSucceeded);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -161,13 +160,29 @@ await AssertHoverMatches(documentItem, (0, 10),
     }
 
 
+    [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+    public async Task MeaningfulMessageForFailingPreconditions() {
+      var documentItem = await GetDocumentItem(@"
+method Test1() {
+    Test2(0);  // Hover #1
+}
+
+method Test2(i: int)
+  requires i > 0 {
+
+}", "testfile.dfy", CompilationStatus.VerificationFailed);
+      await AssertHoverMatches(documentItem, (1, 10),
+        @"???
+Failing precondition:???"
+      );
+    }
+
     [TestMethod, Timeout(MaxTestExecutionTimeMs)]
     public async Task MeaningfulMessageWhenMethodWithOneAssert() {
       var documentItem = await GetDocumentItem(@"
 method f(x: int) {
   assert false;
 }", "testfile1.dfy", CompilationStatus.VerificationFailed);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -184,7 +199,6 @@ method f(x: int) {
   assert false;
   assert false;
 }", "testfile2.dfy", CompilationStatus.VerificationFailed);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 7),
         @"**Verification performance metrics for method f**:
 
@@ -211,7 +225,6 @@ requires p > 0 && q > 0
   }
   assert {:split_here} true;
 } ", "testfileSlow.dfy", CompilationStatus.VerificationFailed);
-      await Task.Delay(100); // Just time for the diagnostics to be updated
       await AssertHoverMatches(documentItem, (0, 22),
         @"**Verification performance metrics for method SquareRoot2NotRational**:
 
@@ -229,6 +242,9 @@ private async Task<TextDocumentItem> GetDocumentItem(string source, string filen
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var lastStatus = await WaitUntilDafnyFinishes(documentItem);
       Assert.AreEqual(expectedStatus, lastStatus);
+      foreach (var document in Documents.Documents) {
+        await document.LastDocument;
+      }
       return documentItem;
     }
 

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

@@ -182,8 +182,8 @@ private string GetAssertionInformation(Position position, AssertionVerificationT
 
 
       var currentlyHoveringPostcondition =
-        !(assertionNode.GetCounterExample() is ReturnCounterexample returnCounterexample2 &&
-          returnCounterexample2.FailingReturn.tok.GetLspRange().Contains(position));
+        assertionNode.GetCounterExample() is ReturnCounterexample returnCounterexample2 &&
+          !returnCounterexample2.FailingReturn.tok.GetLspRange().Contains(position);
 
       var obsolescence = assertionNode.StatusCurrent switch {
         CurrentStatus.Current => "",
@@ -248,6 +248,12 @@ string GetDescription(Boogie.ProofObligationDescription? description) {
           : "");
       }
 
+      if (assertionNode.GetCounterExample() is CallCounterexample) {
+        information += "  \n" + (assertionNode.SecondaryPosition != null
+          ? $"Failing precondition: {Path.GetFileName(assertionNode.Filename)}({assertionNode.SecondaryPosition.Line + 1}, {assertionNode.SecondaryPosition.Character + 1})"
+          : "");
+      }
+
       return information;
     }