Fixed test annotations and un-ignored some more tests

viperproject · Jan 21, 2024 · d5df500 · d5df500
1 parent f3fd473
commit d5df500
Show file tree

Hide file tree

Showing 7 changed files with 10 additions and 10 deletions.
diff --git a/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr b/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr
@@ -29,6 +29,7 @@ method m2(xs: Set[Ref], ys: Set[Ref], z: Ref) {
     assume y.f == 0
     fold p1(y)
     //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/000/)
+    //:: MissingOutput(assert.failed:assertion.false, /carbon/issue/000/)
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert y != z
 }
@@ -42,7 +43,7 @@ method m3(xs: Seq[Ref], y: Ref, zs: Seq[Ref]) {
         assume !(z in xs)
         package acc(z.f) --* acc(y.f)
         assume forall x: Ref :: {acc(x.f) --* acc(y.f)} x in zs ==> x != y
-        //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243)
+        //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/000/)
         assert z != y
 }
 

diff --git a/src/test/resources/all/heap-dependent_triggers/triggerWand.vpr b/src/test/resources/all/heap-dependent_triggers/triggerWand.vpr
@@ -1,7 +1,5 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: IgnoreFile(/carbon/issue/255/)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
 
 field f: Int
 
@@ -19,6 +17,7 @@ method m2(xs: Set[Ref], ys: Set[Ref]) {
     inhale forall x: Ref, y: Ref :: x in xs && y in ys ==> acc(x.f) --* acc(y.f)
     inhale forall x: Ref, y: Ref :: {acc(x.f) --* acc(y.f)} x in xs && y in ys ==> x != y
 
+    //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/257/)
     assert forperm x: Ref, y: Ref [acc(x.f) --* acc(y.f)] :: x != y
 }
 
@@ -34,5 +33,6 @@ method m3(xs: Set[Ref], ys: Set[Ref]) {
     assume b in ys
 
     assert perm(acc(a.f) --* acc(b.f)) == write
+    //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/257/)
     assert a != b
 }
diff --git a/src/test/resources/all/impure_assume/assume10QPwand.vpr b/src/test/resources/all/impure_assume/assume10QPwand.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/255/)
 
 field f: Int
 
@@ -44,6 +43,7 @@ method m(xs: Set[Ref], ys: Set[Ref], zs: Set[Ref],
   assume CONTAINED(a, xs1, b, ys1, c, zs1)
   assume CONTAINED(a, xs2, b, ys2, c, zs2)
 
+  //:: UnexpectedOutput(assert.failed:wand.not.found, /carbon/issue/257/)
   assert WAND(a, b, c, q) && WAND(a, b, c, q)
 
   //:: ExpectedOutput(assert.failed:assertion.false)

diff --git a/src/test/resources/all/permission_introspection/forpermPredicatesAdvanced.vpr b/src/test/resources/all/permission_introspection/forpermPredicatesAdvanced.vpr
@@ -16,7 +16,7 @@ method m2(x: Ref, y: Ref, z: Ref) {
     inhale p2(z, y)
     inhale x != z
 
-    //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243)
+    //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243/)
     assert !forperm a: Ref [p2(a,y)] :: a == z
     unfold p2(x,y)
     assert forperm a: Ref [p2(a,y)] :: a == z

diff --git a/src/test/resources/all/permission_introspection/forpermQP.vpr b/src/test/resources/all/permission_introspection/forpermQP.vpr
@@ -14,7 +14,7 @@ field f: Int
        inhale acc(g.f)
        inhale forall a: Ref :: a == g ==> acc(a.f) && a.f < 3
 
-       //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243)
+       //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243/)
        assert !forperm a: Ref [a.f] :: a.f > 3
 
        inhale forall a: Ref :: a == x || a == y ==> a.f == 4

diff --git a/src/test/resources/all/permission_introspection/forpermWands.vpr b/src/test/resources/all/permission_introspection/forpermWands.vpr
@@ -21,7 +21,7 @@ method m2(x: Ref, y: Ref, z: Ref) {
     inhale acc(z.f) --* acc(y.f)
     inhale forperm a: Ref, b: Ref [acc(a.f) --* acc(b.f)] :: a.f > 0 && b.f < 0
 
-    //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243)
+    //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/243/)
     assert x.f > 0
     assert y.f < 0
 

diff --git a/src/test/resources/quantifiedpredicates/basic/partial_permissions.vpr b/src/test/resources/quantifiedpredicates/basic/partial_permissions.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/257/)
 
 field f: Int