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
 }
 
@@ -250,6 +254,4 @@ pure func (b bigEndian) GoString() (res string) { return "binary.BigEndian" }
 // If v is neither of these, Size returns -1.
 // (joao) requires support for the reflect package
 decreases
-func Size(v interface{}) int /*{
-	return dataSize(reflect.Indirect(reflect.ValueOf(v)))
-}*/
+func Size(v interface{}) int

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

@@ -429,7 +429,7 @@ 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(ctx.specification()).at(ctx)
     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/TypeTyping.scala

@@ -89,10 +89,21 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
             noConditionalMeasureErrors(sig.spec.terminationMeasures)
           else noMessages
         }
+        // Pure method signatures in an interface must satisfy the same requirements as pure implementations.
+        // This reuses the shared `wellDefIfPureSpec` checks and, as for pure functions and methods, requires a
+        // termination measure to be provided (unless termination checking of pure members is disabled).
+        val pureSigErrors = t.methSpecs.flatMap { sig =>
+          if (sig.spec.isPure)
+            wellDefIfPureSpec(sig, sig.args, sig.spec) ++
+              error(sig, "Pure interface methods must have termination measures, but none was found.",
+                !config.disableCheckTerminationPureFns && sig.spec.terminationMeasures.isEmpty)
+          else noMessages
+        }
         methodSet.errors(t) ++
           error(t, "Interface declaration contains methods annotated with 'mayInit'.", methodsContainMayInit) ++
           sigsWithWildcardMeasuresErrors ++
           sigsWithConditionalMeasuresErrors ++
+          pureSigErrors ++
           containsRedeclarations(t) // temporary check
       } else {
         isRecursiveInterface

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

@@ -60,11 +60,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 +84,24 @@ 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, and non-variadic arguments. Checks that are
+  // specific to members with a body (e.g., a single pure return expression) or to a particular kind of member
+  // (e.g., `mayInit`, or the requirement to have a termination measure) are added by the callers.
+  // Precondition: `spec.isPure`.
+  private[typing] def wellDefIfPureSpec(node: PCodeRootWithResult, args: Vector[PParameter], spec: PFunctionSpec): Messages = {
+    isSingleResultArg(node) ++
+      isPurePostcondition(spec) ++
+      pureMembersCannotHavePreserves(spec) ++
+      nonVariadicArguments(args)
+  }
+
   private def isSingleResultArg(member: PCodeRootWithResult): Messages = {
     error(member, "For now, pure methods and pure functions must have exactly one result argument", member.result.outs.size != 1)
   }

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,39 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000841
+
+// Issue #841: pure method signatures in an interface must satisfy the same
+// requirements as pure implementations. Requiring a termination measure is
+// gated behind the same flag as for pure functions and methods
+// (`disableCheckTerminationPureFns`), which the regression test suite disables;
+// hence this file exercises the requirements that are always checked: exactly
+// one result parameter, non-variadic parameters, and the rejection of
+// conditional termination measures.
+
+type J interface {
+	// Type error, a pure interface method must have exactly one result parameter.
+	// The error is reported at the start of the method specification.
+	//:: ExpectedOutput(type_error)
+	decreases
+	pure
+	M1(a int)
+
+	// Type error, we do not permit conditional termination measures for members that must terminate.
+	//:: ExpectedOutput(type_error)
+	decreases if a == 42
+	pure
+	M2(a int) int
+
+	// Type error, a pure interface method cannot have variadic parameters.
+	decreases
+	pure
+	//:: ExpectedOutput(type_error)
+	M3(a ...int) int
+}
+
+// Conditional termination measures are likewise rejected for top-level pure functions.
+pure
+//:: ExpectedOutput(type_error)
+decreases _ if b // we syntactically disallow conditional termination measures for members that must terminate
+func f(b bool) bool