Merge pull request #767 from viperproject/meilers_carbon_missing_feat…

…ures_tests Updating test annotations
viperproject · Feb 2, 2024 · 7059da7 · 7059da7
2 parents a4ca89c + 09cf81b
commit 7059da7
Show file tree

Hide file tree

Showing 22 changed files with 28 additions and 48 deletions.
diff --git a/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr b/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr
@@ -1,8 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/257/)
-
 field f: Int
 
 method m1(xs: Set[Ref], y: Ref, zs: Seq[Ref]) {
@@ -31,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
 }
@@ -44,6 +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/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/issues/silicon/0388.vpr b/src/test/resources/all/issues/silicon/0388.vpr
@@ -1,4 +1,3 @@
-//:: IgnoreFile(/carbon/issue/294/)
 
 predicate P()
 

diff --git a/src/test/resources/all/issues/silicon/0493c.vpr b/src/test/resources/all/issues/silicon/0493c.vpr
@@ -2,8 +2,6 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 //:: IgnoreFile(/silver/issue/488/)
-//:: IgnoreFile(/carbon/issue/244/)
-//:: IgnoreFile(/carbon/issue/257/)
 
 field val: Int
 

diff --git a/src/test/resources/all/issues/silicon/0496.vpr b/src/test/resources/all/issues/silicon/0496.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/257/)
 //:: IgnoreFile(/silver/issue/478/)
 
 field val: Int

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

diff --git a/src/test/resources/all/permission_introspection/forpermPredicatesAdvanced.vpr b/src/test/resources/all/permission_introspection/forpermPredicatesAdvanced.vpr
@@ -1,7 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: IgnoreFile(/Carbon/issue/243/)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 method m1(x: Ref, y: Ref) {
@@ -17,6 +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/)
     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
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/Carbon/issue/243/)
 field f: Int
 
    method m1(x: Ref, y: Ref, z: Ref) {
@@ -15,6 +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/)
        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
@@ -1,7 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: IgnoreFile(/Carbon/issue/243/)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 method m1(x: Ref, y: Ref) {
@@ -22,6 +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/)
     assert x.f > 0
     assert y.f < 0
 

diff --git a/src/test/resources/all/permission_introspection/permWandAlias.vpr b/src/test/resources/all/permission_introspection/permWandAlias.vpr
@@ -1,7 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: IgnoreFile(/Carbon/issue/243/)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 field g: Int
 

diff --git a/src/test/resources/all/permission_introspection/permWandApply.vpr b/src/test/resources/all/permission_introspection/permWandApply.vpr
@@ -1,7 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: IgnoreFile(/Carbon/issue/243/)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 field g: Int
 

diff --git a/src/test/resources/all/permission_introspection/permWandInhale.vpr b/src/test/resources/all/permission_introspection/permWandInhale.vpr
@@ -1,7 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: IgnoreFile(/Carbon/issue/243/)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 field g: Int
 

diff --git a/src/test/resources/all/permission_introspection/permWandQP.vpr b/src/test/resources/all/permission_introspection/permWandQP.vpr
@@ -1,7 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-//:: IgnoreFile(/Carbon/issue/243/)
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 field g: Int
 

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

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

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
 

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

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

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

diff --git a/src/test/resources/wands/regression/snapshots.vpr b/src/test/resources/wands/regression/snapshots.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/244/)
 field f: Int
 field g: Int
 field h: Bool
@@ -23,7 +22,6 @@ method test01(x: Ref)
   unfold acc(P(x))
   apply A
   assert acc(x.g) && ((x.f) + (x.g) > 0)
-  //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/110/)
   assert x.g == 1
 }
 
diff --git a/src/test/resources/wands/regression/wand_shapes_simple_exhale.vpr b/src/test/resources/wands/regression/wand_shapes_simple_exhale.vpr
@@ -1,7 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/244/)
 //:: IgnoreFile(/silver/issue/478/)
 
 field f: Ref