Fixed issue 234: Test case linked-list-predicates doesn't reliably terminate.

Author: fabiopakk

src/main/scala/viper/silver/ast/Expression.scala

@@ -478,6 +478,10 @@ case class LabelledOld(exp: Exp, oldLabel: String)(val pos: Position = NoPositio
       Consistency.checkPure(exp)
 }
 
+case object LabelledOld {
+  val LhsOldLabel = "lhs"
+}
+
 // --- Other expressions
 
 case class Let(variable: LocalVarDecl, exp: Exp, body: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Exp with Scope {

src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -339,7 +339,7 @@ object Consistency {
 
         c.copy(insideWandStatus = InsideWandStatus.Yes)
 
-      case po@LabelledOld(_, FastParser.LHS_OLD_LABEL) if !c.insideWandStatus.isInside =>
+      case po@LabelledOld(_, LabelledOld.LhsOldLabel) if !c.insideWandStatus.isInside =>
         s :+= ConsistencyError("Labelled old expressions with \"lhs\" label may only occur inside wands and their proof scripts.", po.pos)
         c
 
@@ -374,7 +374,7 @@ object Consistency {
         s ++= checkWandRelatedOldExpressions(lhs, c.copy(insideWandStatus = InsideWandStatus.Left))
         s ++= checkWandRelatedOldExpressions(rhs, c.copy(insideWandStatus = InsideWandStatus.Right))
 
-      case po @ LabelledOld(_, FastParser.LHS_OLD_LABEL) if !c.insideWandStatus.isRight =>
+      case po @ LabelledOld(_, LabelledOld.LhsOldLabel) if !c.insideWandStatus.isRight =>
           s :+= ConsistencyError("Wands may use the old[lhs]-expression on the rhs and in their proof script only.", po.pos)
     })
     s

src/main/scala/viper/silver/ast/utility/Expressions.scala

@@ -11,7 +11,6 @@ import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Traverse
 import viper.silver.ast.utility.Triggers.TriggerGeneration
 import viper.silver.utility.Sanitizer
-import viper.silver.parser.FastParser
 
 /** Utility methods for expressions. */
 object Expressions {
@@ -65,7 +64,7 @@ object Expressions {
         currentState => //if (depends) PartialFunction.empty // we're done
           //else
         {
-          case LabelledOld(ee, FastParser.LHS_OLD_LABEL) =>
+          case LabelledOld(ee, LabelledOld.LhsOldLabel) =>
             if (treatMagicWandStatesAsCurrentStates)
               go(ee,p,true)
             else