Fix #815

src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala

@@ -93,6 +93,9 @@ trait Enclosing { this: TypeInfoImpl =>
   lazy val isEnclosingDomain: PNode => Boolean =
     down(false){ case _: PDomainType => true }
 
+  lazy val isEnclosingMagicWand: PNode => Boolean =
+    down(false) { case _: PMagicWand => true }
+
   def isGlobalVarDeclaration(n: PVarDecl): Boolean =
     enclosingCodeRoot(n).isInstanceOf[PPackage]
 

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

@@ -7,6 +7,7 @@
 package viper.gobra.frontend.info.implementation.typing.ghost
 
 import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, message, noMessages}
+import viper.gobra.ast.frontend.PLabelNode.lhsLabel
 import viper.gobra.ast.frontend._
 import viper.gobra.frontend.info.base.SymbolTable
 import viper.gobra.frontend.info.base.SymbolTable.{BuiltInMPredicate, GhostTypeMember, MPredicateImpl, MPredicateSpec}
@@ -155,6 +156,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 +170,41 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
         error(n, "Termination measures of loops cannot be conditional.", terminationMeasure.exists(isConditional))
   }
 
+  private[typing] def hasOldExpressionExceptValidWand(n: PExpression): Boolean =
+    (n +: allChildren(n)).exists {
+      case _: POld => true
+      case o: PLabeledOld if o.label.name == lhsLabel => !isEnclosingMagicWand(o)
+      case _: PLabeledOld => true
+      case _ => false
+    }
+
+  private def presFreeOfOld(pres: Vector[PExpression]): Messages = {
+    pres.flatMap { pre =>
+      error(pre, "old(_) expressions cannot occur in preconditions of functions and methods.", hasOldExpressionExceptValidWand(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.", hasOldExpressionExceptValidWand(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.", hasOldExpressionExceptValidWand(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.", hasOldExpressionExceptValidWand(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()