Fix issue #841

src/main/resources/stubs/encoding/binary/binary.gobra

@@ -11,13 +11,16 @@ package binary
 // 16-, 32-, or 64-bit unsigned integers.
 type ByteOrder interface {
 	requires acc(&b[0], _) && acc(&b[1], _)
+	decreases
 	pure Uint16(b []byte) uint16
 
 	requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
+	decreases
 	pure Uint32(b []byte) uint32
 
 	requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _)
 	requires acc(&b[4], _) && acc(&b[5], _) && acc(&b[6], _) && acc(&b[7], _)
+	decreases
 	pure Uint64(b []byte) uint64
 
 	requires acc(&b[0]) && acc(&b[1])
@@ -37,6 +40,7 @@ type ByteOrder interface {
 	decreases
 	PutUint64(b []byte, uint64)
 
+	decreases
 	pure String() string
 }
 

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -436,7 +436,12 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
   override def visitMethodSpec(ctx: GobraParser.MethodSpecContext): PMethodSig = {
     val ghost = has(ctx.GHOST())
     val spec = if (ctx.specification() != null)
-      visitSpecification(ctx.specification())
+      // `visitSpecification` does not position the node it returns; usually, this is done by `visitChildren` of
+      // the enclosing context, which we bypass here. Without this, the specification of an interface method
+      // signature would be the only `PFunctionSpec` in the AST without a position, so any error reported on it
+      // would be rendered without a source location. We position it at the `specification` context, exactly as
+      // `visitChildren` does for the specs of function and method declarations.
+      visitSpecification(ctx.specification()).at(ctx.specification())
     else
       PFunctionSpec(Vector.empty, Vector.empty, Vector.empty).at(ctx)
     // The name of each explicitly specified method must be unique and not blank.

src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala

@@ -26,16 +26,14 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
         wellDefIfPureFunction(n) ++
         wellDefIfInitBlock(n) ++
         wellDefIfMain(n) ++
-        wellFoundedIfNeeded(n) ++
-        atomicMemberIsWellFormed(n) ++
-        noConditionalMeasureIfGhostOrPure(n)
+        wellFoundedIfGhost(n) ++
+        atomicMemberIsWellFormed(n)
     case m: PMethodDecl =>
       wellDefVariadicArgs(m.args) ++
         isReceiverType.errors(miscType(m.receiver))(member) ++
         wellDefIfPureMethod(m) ++
-        wellFoundedIfNeeded(m) ++
-        atomicMemberIsWellFormed(m) ++
-        noConditionalMeasureIfGhostOrPure(m)
+        wellFoundedIfGhost(m) ++
+        atomicMemberIsWellFormed(m)
     case b: PConstDecl =>
       b.specs.flatMap(wellDefConstSpec)
     case g: PVarDecl if isGlobalVarDeclaration(g) =>

src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala

@@ -7,7 +7,7 @@
 package viper.gobra.frontend.info.implementation.typing
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error}
-import viper.gobra.ast.frontend.{PTerminationMeasure, PTupleTerminationMeasure, PWildcardMeasure}
+import viper.gobra.ast.frontend.{PFunctionSpec, PNode, PTerminationMeasure, PTupleTerminationMeasure, PWildcardMeasure}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 /**
@@ -46,6 +46,25 @@ trait TerminationTyping extends BaseTyping { this: TypeInfoImpl =>
         isConditional(m))
     }
 
+  /**
+    * Checks that `spec` guarantees that the member it belongs to terminates on every call, as Gobra
+    * requires of all ghost and pure members: functions, methods, and interface method signatures alike.
+    * The missing-measure error is reported on `node`, which should be the member or signature that
+    * `spec` specifies.
+    *
+    * Note that this does not simply reject the specifications for which `measuresGuaranteeTermination`
+    * does not hold, because that would collapse two distinct problems into one message. Instead, a
+    * missing measure and a conditional measure are reported separately, the latter on the offending
+    * measure itself. Reporting a missing measure is subject to `disableCheckTerminationPureFns`,
+    * whereas conditional measures are always rejected.
+    */
+  private[typing] def mustTerminateErrors(node: PNode, spec: PFunctionSpec): Messages = {
+    val missingMeasureError = error(node,
+      "Ghost and pure functions, methods, and interface methods must have termination measures, but none was found.",
+      !config.disableCheckTerminationPureFns && spec.terminationMeasures.isEmpty)
+    missingMeasureError ++ noConditionalMeasureErrors(spec.terminationMeasures)
+  }
+
   private[typing] def hasSameMeasureType(measures: Vector[PTerminationMeasure]): Boolean = {
     val tupleMeasureTypes = measures
       .collect { case ttm: PTupleTerminationMeasure => ttm }

src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala

@@ -84,19 +84,27 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
             case _ => noMessages
           }
         }
-        val sigsWithConditionalMeasuresErrors = t.methSpecs.flatMap { sig =>
-          if (sig.isGhost || sig.spec.isPure)
-            noConditionalMeasureErrors(sig.spec.terminationMeasures)
+        // Ghost method signatures must be guaranteed to terminate, exactly like ghost functions and methods.
+        // Pure signatures, ghost or not, are covered by `pureSigErrors` below instead.
+        val ghostSigsMustTerminateErrors = t.methSpecs.flatMap { sig =>
+          if (sig.isGhost && !sig.spec.isPure) mustTerminateErrors(sig, sig.spec)
           else noMessages
         }
         val interfaceMethodsNotAtomic = t.methSpecs.flatMap { sig =>
           error(sig, s"Interface methods cannot be marked as atomic.", sig.spec.isAtomic)
         }
+        // Pure method signatures in an interface must satisfy the same requirements as pure implementations,
+        // including being guaranteed to terminate. This is checked uniformly in `wellDefIfPureSpec`.
+        val pureSigErrors = t.methSpecs.flatMap { sig =>
+          if (sig.spec.isPure) wellDefIfPureSpec(sig, sig.args, sig.spec)
+          else noMessages
+        }
         methodSet.errors(t) ++
           error(t, "Interface declaration contains methods annotated with 'mayInit'.", methodsContainMayInit) ++
           interfaceMethodsNotAtomic ++
           sigsWithWildcardMeasuresErrors ++
-          sigsWithConditionalMeasuresErrors ++
+          ghostSigsMustTerminateErrors ++
+          pureSigErrors ++
           containsRedeclarations(t) // temporary check
       } else {
         isRecursiveInterface

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala

@@ -28,30 +28,15 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
         nonVariadicArguments(args)
   }
 
-  private[typing] def wellFoundedIfNeeded(member: PMember): Messages = {
+  // Ghost functions and methods must be guaranteed to terminate. Pure members, whether ghost or not, are
+  // checked uniformly in `wellDefIfPureSpec`, which is why they are excluded here.
+  private[typing] def wellFoundedIfGhost(member: PMember): Messages = {
     val spec = member match {
       case m: PMethodDecl => m.spec
       case f: PFunctionDecl => f.spec
       case _ => Violation.violation("Unexpected member type")
     }
-    val hasMeasureIfNeeded =
-      if (spec.isPure || isEnclosingGhost(member))
-        config.disableCheckTerminationPureFns || spec.terminationMeasures.nonEmpty
-      else
-        true
-    val needsMeasureError =
-      error(member, "All pure or ghost functions and methods must have termination measures, but none was found for this member.", !hasMeasureIfNeeded)
-    needsMeasureError
-  }
-
-  private[typing] def noConditionalMeasureIfGhostOrPure(member: PMember): Messages = {
-    val spec = member match {
-      case m: PMethodDecl => m.spec
-      case f: PFunctionDecl => f.spec
-      case _ => return noMessages
-    }
-    if (spec.isPure || isEnclosingGhost(member))
-      noConditionalMeasureErrors(spec.terminationMeasures)
+    if (isEnclosingGhost(member) && !spec.isPure) mustTerminateErrors(member, spec)
     else noMessages
   }
 
@@ -60,11 +45,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = {
     if (member.spec.isPure) {
-      isSingleResultArg(member) ++
+      wellDefIfPureSpec(member, member.args, member.spec) ++
         isSinglePureReturnExpr(member) ++
-        isPurePostcondition(member.spec) ++
-        pureMembersCannotHavePreserves(member.spec) ++
-        nonVariadicArguments(member.args) ++
         error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages
   }
@@ -87,15 +69,25 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefIfPureFunction(member: PFunctionDecl): Messages = {
     if (member.spec.isPure) {
-      isSingleResultArg(member) ++
+      wellDefIfPureSpec(member, member.args, member.spec) ++
         isSinglePureReturnExpr(member) ++
-        isPurePostcondition(member.spec) ++
-        pureMembersCannotHavePreserves(member.spec) ++
-        nonVariadicArguments(member.args) ++
         error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit)
     } else noMessages
   }
 
+  // Well-definedness checks shared by pure functions, pure methods, and pure interface method signatures:
+  // exactly one result, pure postconditions, no `preserves` clauses, non-variadic arguments, and a termination
+  // measure that guarantees termination. Checks specific to members with a body (e.g., a single pure return
+  // expression) or to a particular kind of member (e.g., `mayInit`) are added by the callers.
+  private[typing] def wellDefIfPureSpec(node: PCodeRootWithResult, args: Vector[PParameter], spec: PFunctionSpec): Messages = {
+    Violation.violation(spec.isPure, "wellDefIfPureSpec may only be called for the specification of a pure member.")
+    isSingleResultArg(node) ++
+      isPurePostcondition(spec) ++
+      pureMembersCannotHavePreserves(spec) ++
+      nonVariadicArguments(args) ++
+      mustTerminateErrors(node, spec)
+  }
+
   private[typing] def atomicMemberIsWellFormed(member: PMember): Messages = {
     val (bodyOpt, spec) = member match {
       case f: PFunctionDecl => (f.body, f.spec)

src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra

@@ -0,0 +1,73 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package ghost_and_pure_members_need_measures
+
+// Ghost and pure members must be guaranteed to terminate on every call. Following issue #841, this
+// includes the method signatures declared in an interface, which used to be exempt. Unlike the main
+// regression test suite, the files in this directory are checked with `disableCheckTerminationPureFns`
+// disabled.
+
+type T struct{ f int }
+
+// Type error, a pure function must have a termination measure.
+//:: ExpectedOutput(type_error)
+pure func missingMeasureFunc(a int) int {
+	return a
+}
+
+// Type error, a pure method must have a termination measure.
+//:: ExpectedOutput(type_error)
+pure func (t T) missingMeasureMethod(a int) int {
+	return a
+}
+
+// Type error, a ghost function must have a termination measure.
+ghost
+//:: ExpectedOutput(type_error)
+func missingMeasureGhostFunc(a int) int {
+	return a
+}
+
+// Type error, a ghost method must have a termination measure.
+ghost
+//:: ExpectedOutput(type_error)
+func (t T) missingMeasureGhostMethod(a int) int {
+	return a
+}
+
+type I interface {
+	// Type error, a pure interface method must have a termination measure.
+	//:: ExpectedOutput(type_error)
+	pure MissingMeasurePure(a int) int
+
+	// Type error, a ghost interface method must have a termination measure.
+	//:: ExpectedOutput(type_error)
+	ghost MissingMeasureGhost(a int)
+
+	decreases
+	pure HasMeasurePure(a int) int
+
+	ghost
+	decreases
+	HasMeasureGhost(a int)
+
+	// An interface method that is neither ghost nor pure need not terminate.
+	NeedNotTerminate(a int)
+}
+
+decreases
+pure func withMeasureFunc(a int) int {
+	return a
+}
+
+decreases
+pure func (t T) withMeasureMethod(a int) int {
+	return a
+}
+
+ghost
+decreases
+func withMeasureGhostFunc(a int) int {
+	return a
+}

src/test/resources/regressions/features/interfaces/embeddedInterfaces-fail3.gobra

@@ -10,14 +10,14 @@ type foo interface {
 }
 
 type bar interface {
-	pure g()
+	pure g() int
 }
 
 type test int
 
 func (x test) f()
 
-func (x test) g()
+func (x test) g() int
 
 //:: ExpectedOutput(type_error)
 test implements foo

src/test/resources/regressions/issues/000841.gobra

@@ -0,0 +1,45 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000841
+
+// Issue #841: pure method signatures declared in an interface must satisfy the same requirements as
+// pure functions and pure methods. The requirement of carrying a termination measure is gated behind
+// `disableCheckTerminationPureFns`, which this test suite enables; that case is covered by the tests
+// in `src/test/resources/check_termination` instead.
+
+type J interface {
+	// Type error, a pure member must have exactly one result parameter.
+	//:: ExpectedOutput(type_error)
+	decreases
+	pure NoResult(a int)
+
+	// Type error, a pure member must have exactly one result parameter.
+	//:: ExpectedOutput(type_error)
+	decreases
+	pure TwoResults(a int) (int, int)
+
+	decreases
+	// Type error, a pure member cannot have variadic parameters.
+	//:: ExpectedOutput(type_error)
+	pure Variadic(a ...int) int
+
+	// Type error, a pure member cannot have preserves clauses.
+	//:: ExpectedOutput(type_error)
+	preserves a > 0
+	decreases
+	pure Preserves(a int) int
+
+	// Type error, the postconditions of a pure member must be pure.
+	//:: ExpectedOutput(type_error)
+	ensures acc(x)
+	decreases
+	pure ImpurePostcondition(x *int) int
+}
+
+// A pure method signature that satisfies all of the requirements above is accepted.
+type K interface {
+	ensures res >= a
+	decreases
+	pure WellFormed(a int) (res int)
+}

src/test/scala/viper/gobra/GobraCheckTerminationTests.scala

@@ -0,0 +1,32 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2026 ETH Zurich.
+
+package viper.gobra
+
+import org.bitbucket.inkytonik.kiama.util.Source
+import viper.gobra.frontend.Config
+
+/**
+  * Runs the test files in `src/test/resources/check_termination` with `disableCheckTerminationPureFns`
+  * disabled, i.e., with the requirement that all pure and ghost members carry a termination measure.
+  *
+  * The main regression test suite ([[GobraTests]]) sets `disableCheckTerminationPureFns` to `true`,
+  * because adding termination measures to all of its test files is still pending work. Note that an
+  * in-file configuration (`// ##(...)`) cannot be used to opt out of that setting, as configurations
+  * are merged by taking the disjunction of the boolean flags. This suite exists so that the
+  * requirement itself can be tested; test files that are unrelated to termination checking belong to
+  * the main regression test suite instead.
+  */
+class GobraCheckTerminationTests extends GobraTests {
+  val checkTerminationPropertyName = "GOBRATESTS_CHECK_TERMINATION_DIR"
+
+  val checkTerminationDir: String = System.getProperty(checkTerminationPropertyName, "check_termination")
+
+  override val testDirectories: Seq[String] = Vector(checkTerminationDir)
+
+  override protected def getConfig(source: Source): Config =
+    super.getConfig(source).copy(disableCheckTerminationPureFns = false)
+}