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/ast/frontend/Ast.scala

@@ -874,9 +874,15 @@ object PGhostifier {
   * Termination Measures
   */
 
-sealed trait PTerminationMeasure extends PNode
-case class PWildcardMeasure(cond: Option[PExpression]) extends PTerminationMeasure
-case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PExpression]) extends PTerminationMeasure
+sealed trait PTerminationMeasure extends PNode {
+  val isConditional: Boolean
+}
+case class PWildcardMeasure(cond: Option[PExpression]) extends PTerminationMeasure {
+  override val isConditional: Boolean = cond.nonEmpty
+}
+case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PExpression]) extends PTerminationMeasure {
+  override val isConditional: Boolean = cond.nonEmpty
+}
 
 /**
   * Specification

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

@@ -428,7 +428,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, 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,13 +26,11 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl =>
       wellDefVariadicArgs(n.args) ++
         wellDefIfPureFunction(n) ++
         wellDefIfInitBlock(n) ++
-        wellDefIfMain(n) ++
-        wellFoundedIfNeeded(n)
+        wellDefIfMain(n)
     case m: PMethodDecl =>
       wellDefVariadicArgs(m.args) ++
         isReceiverType.errors(miscType(m.receiver))(member) ++
-        wellDefIfPureMethod(m) ++
-        wellFoundedIfNeeded(m)
+        wellDefIfPureMethod(m)
     case b: PConstDecl =>
       b.specs.flatMap(wellDefConstSpec)
     case g: PVarDecl if isGlobalVarDeclaration(g) =>

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

@@ -66,7 +66,9 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>
     case t: PInterfaceType =>
       val isRecursiveInterface = error(t, "invalid recursive interface", cyclicInterfaceDef(t))
       if (isRecursiveInterface.isEmpty) {
+        val wellDefIfPureSig = t.methSpecs.flatMap { sig => wellDefIfPureSpec(sig.spec, sig.args, sig.result) }
         addressableMethodSet(InterfaceT(t, this)).errors(t) ++
+          wellDefIfPureSig ++
           containsRedeclarations(t) // temporary check
       } else {
         isRecursiveInterface

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

@@ -7,17 +7,20 @@
 package viper.gobra.frontend.info.implementation.typing.ghost
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages}
-import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMember, PMPredicateDecl, PMethodDecl, PMethodImplementationProof, PParameter, PReturn, PVariadicType, PWithBody}
+import viper.gobra.ast.frontend._
 import viper.gobra.frontend.info.base.SymbolTable.{MPredicateSpec, MethodImpl, MethodSpec}
 import viper.gobra.frontend.info.base.Type.{InterfaceT, Type, UnknownType}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.BaseTyping
-import viper.gobra.util.Violation
 
 trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefGhostMember(member: PGhostMember): Messages = member match {
-    case PExplicitGhostMember(_) => noMessages
+    case PExplicitGhostMember(m) => m match {
+      case f: PFunctionDecl => wellFoundedIfNeeded(f.spec)
+      case m: PMethodDecl => wellFoundedIfNeeded(m.spec)
+      case _ => noMessages
+    }
 
     case PFPredicateDecl(_, args, body) =>
       body.fold(noMessages)(assignableToSpec) ++ nonVariadicArguments(args)
@@ -28,28 +31,38 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
         nonVariadicArguments(args)
   }
 
-  private[typing] def wellFoundedIfNeeded(member: PMember): Messages = {
-    val spec = member match {
-      case m: PMethodDecl => m.spec
-      case f: PFunctionDecl => f.spec
-      case _ => Violation.violation("Unexpected member type")
+  // spec must come from a ghost or pure function
+  private[typing] def wellFoundedIfNeeded(spec: PFunctionSpec): Messages = {
+    val needsMeasure = !config.disableCheckTerminationPureFns
+    if (needsMeasure) {
+      isValidMeasureForGhostOrPure(spec)
+    } else noMessages
+  }
+
+  private def isValidMeasureForGhostOrPure(spec: PFunctionSpec): Messages = {
+    // TODO: eventually, we should deprecate the flag `config.disableCheckTerminationPureFns`
+    val hasTerminationMeasureErrors =
+      error(spec, s"Pure and ghost functions and methods must have termination measures.",
+        spec.terminationMeasures.isEmpty)
+    // (João) Conditional termination measures are a very rarely used feature. They allow defining termination measures
+    // case-per-case. However, for pure or ghost functions and methods, we need to show that all conditions provided
+    // do cover all possible inputs, otherwise the function is not guaranteed to terminate. Implementing such a
+    // check would not be hard, but it would be more cumbersome (and in general, less efficient) than this syntactic check.
+    // If this feature is requested, I am happy to implement the more complete check, but for now, I will stick to
+    // this syntactic check.
+    val hasConditionalTerminationMeasureErrors = {
+      val conditionalMeasure = spec.terminationMeasures.find(_.isConditional)
+      conditionalMeasure match {
+        case Some(n) => error(n, "Conditional termination measures are not allowed in pure members.")
+        case None => noMessages
+      }
     }
-    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
+    hasTerminationMeasureErrors ++ hasConditionalTerminationMeasureErrors
   }
 
   private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = {
     if (member.spec.isPure) {
-      isSingleResultArg(member) ++
-        isSinglePureReturnExpr(member) ++
-        isPurePostcondition(member.spec) ++
-        nonVariadicArguments(member.args)
+      wellDefIfPureSpec(member.spec, member.args, member.result) ++ isSinglePureReturnExpr(member)
     } else noMessages
   }
 
@@ -61,15 +74,23 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
 
   private[typing] def wellDefIfPureFunction(member: PFunctionDecl): Messages = {
     if (member.spec.isPure) {
-      isSingleResultArg(member) ++
-        isSinglePureReturnExpr(member) ++
-        isPurePostcondition(member.spec) ++
-        nonVariadicArguments(member.args)
+      wellDefIfPureSpec(member.spec, member.args, member.result) ++ isSinglePureReturnExpr(member)
     } else noMessages
   }
 
-  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)
+  // This implements checks that are common to pure functions and pure methods. Checks that are specific to either
+  // (e.g., checks that may depend on the receiver of a method) should be implemented elsewhere.
+  private[typing] def wellDefIfPureSpec(spec: PFunctionSpec, args: Vector[PParameter], result: PResult) : Messages = {
+    if (spec.isPure) {
+      isSingleResultArg(result) ++
+        isPurePostcondition(spec) ++
+        nonVariadicArguments(args) ++
+        wellFoundedIfNeeded(spec)
+    } else noMessages
+  }
+
+  private def isSingleResultArg(result: PResult): Messages = {
+    error(result, "For now, pure methods and pure functions must have exactly one result argument", result.outs.size != 1)
   }
 
   private def isSinglePureReturnExpr(member: PWithBody): Messages = {
@@ -93,6 +114,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
     p: PParameter => error(p, s"Pure members cannot have variadic arguments, but got $p", p.typ.isInstanceOf[PVariadicType])
   }
 
+
+
   override lazy val localImplementationProofs: Vector[(Type, InterfaceT, Vector[String], Vector[String])] = {
     val implementationProofs = tree.root.programs.flatMap(_.declarations.collect{ case m: PImplementationProof => m})
     implementationProofs.flatMap { ip =>

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

@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000841
+
+type J interface {
+	// Type error, pure function does not have termination measures.
+	//:: ExpectedOutput(type_error)
+	pure
+	// Type error, pure function cannot have variadic parameters.
+	//:: ExpectedOutput(type_error)
+	M(a ...int) int
+}
+
+pure
+//:: ExpectedOutput(type_error)
+decreases _ if b
+func f(b bool) bool