Add UnexpectedOutput annotations for Carbon.

viperproject · May 13, 2024 · 6374709 · 6374709
1 parent 2f700d3
commit 6374709
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 0 deletions.
diff --git a/src/test/resources/wands/snap_functions/test01.vpr b/src/test/resources/wands/snap_functions/test01.vpr
@@ -6,6 +6,7 @@ method test01a(x: Ref)
 
     package true --* acc(x.b)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.b)) in x.b
 }
 
@@ -26,6 +27,7 @@ method test01c(x: Ref)
 
     package true --* acc(x.b)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.b)) in x.b
 
     apply true --* acc(x.b)
@@ -39,6 +41,7 @@ method test01d(x: Ref, a: Bool)
 
     package true --* acc(x.b)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.b)) in x.b == a
 
     apply true --* acc(x.b)

diff --git a/src/test/resources/wands/snap_functions/test02.vpr b/src/test/resources/wands/snap_functions/test02.vpr
@@ -6,6 +6,7 @@ method test02a(x: Ref)
 
     package true --* acc(x.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.f)) in x.f == 42
 }
 
@@ -26,6 +27,7 @@ method test02c(x: Ref)
 
     package true --* acc(x.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.f)) in x.f == 42
 
     apply true --* acc(x.f)
@@ -39,6 +41,7 @@ method test02d(x: Ref, a: Int)
 
     package true --* acc(x.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.f)) in x.f == a
 
     apply true --* acc(x.f)

diff --git a/src/test/resources/wands/snap_functions/test04.vpr b/src/test/resources/wands/snap_functions/test04.vpr
@@ -6,6 +6,7 @@ method test04a(x: Ref, y: Ref)
 
     package acc(x.f) --* acc(x.f) && acc(y.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
 }
 
@@ -26,6 +27,7 @@ method test04c(x: Ref, y: Ref)
 
     package acc(x.f) --* acc(x.f) && acc(y.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
 
     apply acc(x.f) --* acc(x.f) && acc(y.f)
@@ -39,6 +41,7 @@ method test04d(x: Ref, y: Ref, a: Int, b: Int)
 
     package acc(x.f) --* acc(x.f) && acc(y.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == a && y.f == b
 
     apply acc(x.f) --* acc(x.f) && acc(y.f)

diff --git a/src/test/resources/wands/snap_functions/test09.vpr b/src/test/resources/wands/snap_functions/test09.vpr
@@ -4,6 +4,7 @@ method test09a(x: Ref, y: Ref)
     requires acc(x.f) && x.f == 42
     requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
 {
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37) in y.f == 37
 }
 

diff --git a/src/test/resources/wands/snap_functions/test10.vpr b/src/test/resources/wands/snap_functions/test10.vpr
@@ -26,5 +26,6 @@ method test10b(x: Ref)
 
     apply acc(x.f) --* foo(x)
 
+    //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/216/)
     assert foo(x) && unfolding foo(x) in x.f == 42
 }
diff --git a/src/test/resources/wands/snap_functions/test11.vpr b/src/test/resources/wands/snap_functions/test11.vpr
@@ -26,6 +26,7 @@ function sorted(start: Ref) : Bool
 
 method append_it(l1 : Ref, l2: Ref)
   requires List(l1) && List(l2) && l2 != null
+  //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/000/)
   ensures List(l1) && elems(l1) == old(elems(l1) ++ elems(l2))
 {
   unfold List(l1)
@@ -54,6 +55,7 @@ method append_it(l1 : Ref, l2: Ref)
       tmp := tmp.next
       index := index + 1
 
+      //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/000/)
       package List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
       {
         fold List(prev)