From 8668fbe960fe40fb2a4c509c3582534573512b16 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Wed, 8 Jul 2026 02:00:54 +0200
Subject: [PATCH] Reporting labels that declare invariants but aren't loop
 heads

---
 silver                                        |  2 +-
 .../modules/impls/DefaultLoopModule.scala     | 23 +++++++++++++++++--
 .../viper/carbon/verifier/Verifier.scala      |  6 +++++
 3 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/silver b/silver
index 433555e1..2eafc78d 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 433555e1f0453d3248285db240a9289a4e31b0b6
+Subproject commit 2eafc78d51d2cac1118b6efd06e229c71f7536b5
diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala
index a61c89f0..c53a4b7a 100644
--- a/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala
+++ b/src/main/scala/viper/carbon/modules/impls/DefaultLoopModule.scala
@@ -9,7 +9,8 @@ import viper.carbon.modules.components.StmtComponent
 import viper.carbon.utility._
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.cfg.utility.{IdInfo, LoopDetector, LoopInfo}
-import viper.silver.verifier.{PartialVerificationError, errors}
+import viper.silver.reporter.WarningsDuringVerification
+import viper.silver.verifier.{PartialVerificationError, VerifierWarning, errors}
 
 import scala.collection.mutable
 import scala.collection.mutable.Map
@@ -83,10 +84,27 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp
       initializeMethodWithGotos(m)
     } else {
       useLoopDetector = false
+      // Without gotos there are no loops formed by jumps to labels, so no label can be a loop head and all label
+      // invariants are ignored.
+      reportIgnoredLabelInvariants(m.body.fold(Seq.empty[sil.Label])(_.deepCollect {
+        case label@sil.Label(_, invs) if invs.nonEmpty => label
+      }))
       m
     }
   }
 
+  /**
+    * Reports a warning for each of the given labels, which declare invariants but are not loop heads, such that
+    * their invariants are ignored.
+    */
+  private def reportIgnoredLabelInvariants(labels: Seq[sil.Label]): Unit = {
+    if (labels.nonEmpty) {
+      val warnings = labels.map(label =>
+        VerifierWarning(s"Label ${label.name} declares an invariant, but is not the head of a loop. The invariant will be ignored.", label.pos))
+      verifier.reporter report WarningsDuringVerification(warnings)
+    }
+  }
+
   private def initializeMethodWithGotos(m: sil.Method): sil.Method = {
     def isComposite(s: sil.Stmt): Boolean = {
       s match {
@@ -271,7 +289,8 @@ class DefaultLoopModule(val verifier: Verifier) extends LoopModule with StmtComp
               rewriteDummyStatements, sil.utility.rewriter.Traverse.BottomUp
             ).asInstanceOf[sil.Seqn]
 
-          val (loopInfoBody, loopToWrittenVarsResult) = LoopDetector.detect(normalizedBody, true, true)
+          val (loopInfoBody, loopToWrittenVarsResult, labelsWithIgnoredInvariants) = LoopDetector.detect(normalizedBody, true, true)
+          reportIgnoredLabelInvariants(labelsWithIgnoredInvariants)
           loopToWrittenVars = loopToWrittenVarsResult.get
           initializeMappings(loopInfoBody)
           captureRelevantNextStmts(loopInfoBody, Seq())
diff --git a/src/main/scala/viper/carbon/verifier/Verifier.scala b/src/main/scala/viper/carbon/verifier/Verifier.scala
index 9af97523..b6ab4fda 100644
--- a/src/main/scala/viper/carbon/verifier/Verifier.scala
+++ b/src/main/scala/viper/carbon/verifier/Verifier.scala
@@ -9,6 +9,7 @@ package viper.carbon.verifier
 import viper.silver.{ast => sil}
 import viper.carbon.modules._
 import viper.carbon.boogie.Namespace
+import viper.silver.reporter.Reporter
 
 /**
  * A verifier for Viper in Carbon (defines what modules need to be available).
@@ -66,6 +67,11 @@ trait Verifier {
    */
   def freshNamespace(name: String): Namespace
 
+  /**
+   * The reporter used to emit messages (e.g., warnings) during the translation and verification.
+   */
+  def reporter: Reporter
+
   /**
    * The program currently being verified.
    */