Merge pull request #695 from viperproject/meilers_labelled_old_trigger

Labelled old in triggers

Author: marcoeilers

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

@@ -229,6 +229,7 @@ object Consistency {
   def validTrigger(e: Exp, program: Program): Boolean = {
     e match {
       case Old(nested) => validTrigger(nested, program) // case corresponds to OldTrigger node
+      case LabelledOld(nested, _) => validTrigger(nested, program)
       case wand: MagicWand => wand.subexpressionsToEvaluate(program).forall(e => !e.existsDefined {case _: ForbiddenInTrigger => })
       case _ : PossibleTrigger | _: FieldAccess | _: PredicateAccess => !e.existsDefined { case _: ForbiddenInTrigger => }
       case _ => false

src/test/resources/all/issues/silicon/0509b.vpr

@@ -0,0 +1,70 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function lookup(r: Ref, i: Int): Int
+  requires acc(r.f)
+
+
+function lookup2(r: Ref, i: Int): Int
+  requires acc(r.f)
+
+method main(r1: Ref, r2: Ref)
+    requires acc(r1.f) && acc(r2.f)
+{
+  assume r1.f == 1
+  exhale acc(r1.f) && acc(r2.f)
+  inhale acc(r1.f) && acc(r2.f)
+  assume r1.f == 3
+  var s: Set[Ref]
+  s := Set(r1, r2)
+  assume lookup(r1, 5) > 3
+  label before
+  exhale acc(r1.f) && acc(r2.f)
+  inhale acc(r1.f) && acc(r2.f)
+  assume r1.f == 4
+  assume forall i: Int :: { old[before](lookup(r1, i)) } lookup2(r1, i) == old[before](lookup(r1, i))
+
+  assert lookup2(r1, 5) > 2
+}
+
+method main_fail_1(r1: Ref, r2: Ref)
+    requires acc(r1.f) && acc(r2.f)
+{
+  assume r1.f == 1
+  exhale acc(r1.f) && acc(r2.f)
+  inhale acc(r1.f) && acc(r2.f)
+  assume r1.f == 3
+  var s: Set[Ref]
+  s := Set(r1, r2)
+  assume lookup(r1, 5) > 3
+  label before
+  exhale acc(r1.f) && acc(r2.f)
+  inhale acc(r1.f) && acc(r2.f)
+  assume r1.f == 4
+  assume forall i: Int :: { lookup(r1, i) } lookup2(r1, i) == old[before](lookup(r1, i))
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert lookup2(r1, 5) > 2
+}
+
+method main_fail_2(r1: Ref, r2: Ref)
+    requires acc(r1.f) && acc(r2.f)
+{
+  assume r1.f == 1
+  exhale acc(r1.f) && acc(r2.f)
+  inhale acc(r1.f) && acc(r2.f)
+  assume r1.f == 3
+  var s: Set[Ref]
+  s := Set(r1, r2)
+  assume lookup(r1, 5) > 3
+  label before
+  exhale acc(r1.f) && acc(r2.f)
+  inhale acc(r1.f) && acc(r2.f)
+  assume r1.f == 4
+  assume forall i: Int :: { old(lookup(r1, i)) } lookup2(r1, i) == old[before](lookup(r1, i))
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert lookup2(r1, 5) > 2
+}