Fix: Green gutter icons over constants without RHS

Fixes #5841 Tests have been added
dafny-lang · Oct 18, 2024 · 01b727d · 01b727d
1 parent 8f8f585
commit 01b727d
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 3 deletions.
diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs
@@ -37,6 +37,20 @@ await VerifyTrace(@"
  ? :}", false, intermediates: false);
   }
 
+  [Fact]
+  public async Task ConstantWithoutRhsMarkedAsVerified() {
+    await VerifyTrace(@"
+ | :class Test {
+ | :  const x: int
+ | :
+ | :  method Testing()
+ | :    requires x > 0
+ | :    ensures x != 0
+ | :  {
+ | :  }
+ | :}", false, intermediates: false);
+  }
+
   [Fact]
   public async Task Fields() {
     var markedSource = @"

diff --git a/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs b/Source/DafnyLanguageServer/Workspace/GutterIconAndHoverVerificationDetailsManager.cs
@@ -80,9 +80,8 @@ void AddAndPossiblyMigrateVerificationTree(VerificationTree verificationTree) {
               continue;
             }
 
-            if (member is ConstantField) {
-              var constantHasNoBody = member.RangeToken.EndToken.line == 0;
-              if (constantHasNoBody) {
+            if (member is ConstantField constantField) {
+              if (constantField.Rhs == null) {
                 continue; // Nothing to verify
               }
 

diff --git a/docs/dev/news/5841.fix b/docs/dev/news/5841.fix
@@ -0,0 +1 @@
+Green gutter icons cover constants without RHS