From 2db26d2b31de0f15506c742227ec808648458751 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <MikaelMayer@users.noreply.github.com>
Date: Fri, 18 Oct 2024 07:56:25 -0500
Subject: [PATCH] Fix: Green gutter icons over constants without RHS (#5842)

Fixes #5841
Tests have been added

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 .../SimpleLinearVerificationGutterStatusTester.cs  | 14 ++++++++++++++
 ...GutterIconAndHoverVerificationDetailsManager.cs |  5 ++---
 docs/dev/news/5841.fix                             |  1 +
 3 files changed, 17 insertions(+), 3 deletions(-)
 create mode 100644 docs/dev/news/5841.fix

diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs
index 2ad64631be1..c3ba836b81e 100644
--- 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
index 1c22e7b77db..77d7cd2a214 100644
--- 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
new file mode 100644
index 00000000000..df5fa34687a
--- /dev/null
+++ b/docs/dev/news/5841.fix
@@ -0,0 +1 @@
+Green gutter icons cover constants without RHS