Fix: Explicit assertions no longer considered implicit for code actions

Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs

@@ -1,4 +1,4 @@
-using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using System;
 using OmniSharp.Extensions.LanguageServer.Protocol.Document;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Collections.Generic;
@@ -8,11 +8,10 @@
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Xunit;
 using Xunit.Abstractions;
-using XunitAssertMessages;
 
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.CodeActions {
   public class CodeActionTest : ClientBasedLanguageServerTest {
     private async Task<List<CommandOrCodeAction>> RequestCodeActionAsync(TextDocumentItem documentItem, Range range) {
       var completionList = await client.RequestCodeAction(
         new CodeActionParams {
           TextDocument = documentItem.Uri.GetFileSystemPath(),
@@ -76,6 +75,21 @@
       Assert.Empty(completionList);
     }
 
+    [Fact]
+    public async Task TestAssertFalseNotSuggestingItself() {
+      await TestNoCodeAction(@"
+method NoCodeAction() {
+  assert fal><se;
+}");
+    }
+
+    [Fact]
+    public async Task TestEnsureFalseNotSuggestingItself() {
+      await TestNoCodeAction(@"
+method NoCodeAction() ensures f><alse {
+}", excepted: message => message == "Assert postcondition at return location where it fails");
+    }
+
     [Fact]
     public async Task TestInsertion() {
       await TestCodeAction(@"
@@ -371,6 +385,23 @@
 
     private static readonly Regex NewlineRegex = new Regex("\r?\n");
 
+    private async Task TestNoCodeAction(string source, Func<string, bool> excepted = null) {
+      await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true));
+      MarkupTestFile.GetPositionsAndAnnotatedRanges(source.TrimStart(), out var output, out var positions,
+        out var ranges);
+      var documentItem = await CreateOpenAndWaitForResolve(output);
+      var diagnostics = await GetLastDiagnostics(documentItem);
+      Assert.Equal(0, ranges.Count);
+      foreach (var position in positions) {
+        var completionList = await RequestCodeActionAsync(documentItem, new Range(position, position));
+        completionList = excepted == null
+          ? completionList
+          : completionList.Where(completion =>
+            completion.CodeAction is not { Title: var title } || !excepted(title)).ToList();
+        Assert.Empty(completionList);
+      }
+    }
+
     private async Task TestCodeAction(string source) {
       await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true));
 

Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs

@@ -124,7 +124,7 @@ public override IEnumerable<DafnyCodeActionEdit> GetEdits() {
           assertTree.Finished &&
             assertTree.Range.Intersects(selection) &&
             assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerificationStatus.Inconclusive &&
-            assertTree.GetAssertion()?.Description is ProofObligationDescription description &&
+            assertTree.GetAssertion()?.Description is ProofObligationDescription { IsImplicit: true } description &&
             description.GetAssertedExpr(options) is { } assertedExpr) {
         failingExpressions.Add(assertedExpr);
       }

docs/dev/news/6025.fix

@@ -0,0 +1 @@
+The code action for assertion no longer suggests asserting the same assertion.