Adapting tests

viperproject · Oct 4, 2023 · 67fa155 · 67fa155
1 parent e678cd7
commit 67fa155
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 11 deletions.
diff --git a/src/test/resources/all/issues/carbon/0125.vpr b/src/test/resources/all/issues/carbon/0125.vpr
@@ -1,13 +1,13 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 predicate P(x: Ref) { acc(x.f) }
 
 method test1(x: Ref) {
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   unfold acc(P(x), -(1/2))
 }
 
@@ -16,7 +16,7 @@ method test2(x: Ref) {
   assume p == -(1/2)
 
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   unfold acc(P(x), p)
 }
 

diff --git a/src/test/resources/all/issues/silver/0072.vpr b/src/test/resources/all/issues/silver/0072.vpr
@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 predicate token(x: Ref) {
@@ -16,14 +16,14 @@ method t_plus(x: Ref)
 method t_minus_1(x: Ref)
     requires acc(x.f)
 {
-    //:: ExpectedOutput(fold.failed:negative.permission)
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
     fold acc(token(x), (-1/1))
 }
 
 method t_minus_2(x: Ref)
     requires acc(x.f)
 {
-    //:: ExpectedOutput(fold.failed:negative.permission)
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
     fold acc(token(x), -(1/1))
 }
 
diff --git a/src/test/resources/all/issues/silver/0522.vpr b/src/test/resources/all/issues/silver/0522.vpr
@@ -27,7 +27,7 @@ method test3b(x: Ref, p: Perm) {
 
 method test4(x: Ref, p: Perm) {
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   //:: ExpectedOutput(unfold.failed:insufficient.permission)
   //:: MissingOutput(unfold.failed:insufficient.permission, /Silicon/issue/34/)
   unfold acc(P(x), p)