Fix #815

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

@@ -7,7 +7,7 @@
 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.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PParameter, PReturn, PVariadicType, PWithBody}
 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
@@ -87,6 +87,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
     }
   }
 
+
   private def isPurePostcondition(spec: PFunctionSpec): Messages = (spec.posts ++ spec.preserves) flatMap isPureExpr
 
   private[typing] def nonVariadicArguments(args: Vector[PParameter]): Messages = args.flatMap {

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

@@ -155,6 +155,8 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
       preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++
       pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++
       terminationMeasures.flatMap(wellDefTerminationMeasure) ++
+      presFreeOfOld(n.pres) ++
+      postsFreeOfOldIfPure(n.posts, isPure) ++
       // if has conditional clause, all clauses must be conditional
       // can only have one non-conditional clause
       error(n, "Specifications can either contain one non-conditional termination measure or multiple conditional-termination measures.", terminationMeasures.length > 1 && !terminationMeasures.forall(isConditional)) ++
@@ -167,12 +169,36 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
         error(n, "Termination measures of loops cannot be conditional.", terminationMeasure.exists(isConditional))
   }
 
+  private[typing] def hasOldExpression(n: PExpression): Boolean =
+    (n +: allChildren(n)).exists{ e => e.isInstanceOf[POld] || e.isInstanceOf[PLabeledOld]}
+
+  private def presFreeOfOld(pres: Vector[PExpression]): Messages = {
+    pres.flatMap { pre =>
+      error(pre, "old(_) expressions cannot occur in preconditions of functions and methods.", hasOldExpression(pre))
+    }
+  }
+
+  private def postsFreeOfOldIfPure(posts: Vector[PExpression], isPure: Boolean): Messages = {
+    if (isPure)
+      posts.flatMap { post =>
+        error(post, "old(_) expressions cannot occur in postconditions of pure functions.", hasOldExpression(post))
+      }
+    else
+      noMessages
+  }
+
   private def wellDefTerminationMeasure(measure: PTerminationMeasure): Messages = measure match {
     case PTupleTerminationMeasure(tuple, cond) =>
       tuple.flatMap(p => comparableType.errors(exprType(p))(p) ++ isWeaklyPureExpr(p)) ++
-        cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p))
+        cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) ++
+        (tuple ++ cond).flatMap { expr =>
+          error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpression(expr))
+        }
     case PWildcardMeasure(cond) =>
-      cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p))
+      cond.toVector.flatMap(p => assignableToSpec(p) ++ isPureExpr(p)) ++
+        cond.map { expr =>
+          error(expr, "old(_) expressions cannot occur in termination measures.", hasOldExpression(expr))
+        }.getOrElse(noMessages)
   }
 
   private def wellDefClosureSpecInstanceParams(c: PClosureSpecInstance, fArgs: Vector[(PParameter, Type)]): Messages = c match {

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

@@ -0,0 +1,28 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue815
+
+type cell struct {
+	value int
+}
+
+pure
+requires acc(c)
+// old expressions not allowed in postconditions of pure functions
+//:: ExpectedOutput(type_error)
+ensures r == old(c.value)
+decreases
+func read(c *cell) (r int) {
+	return c.value
+}
+
+// old expressions not allowed in preconditions
+//:: ExpectedOutput(type_error)
+requires old(true)
+func oldInPre()
+
+// old expressions not allowed in termination measures
+//:: ExpectedOutput(type_error)
+decreases old(1)
+func oldInDecreasesClause()