Test for Carbon issue #391 (#829)

viperproject · Dec 30, 2024 · 6ddaa1b · 6ddaa1b
1 parent 92c0914
commit 6ddaa1b
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 1 deletion.
diff --git a/src/test/resources/all/issues/carbon/0391.vpr b/src/test/resources/all/issues/carbon/0391.vpr
@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate p()
+
+method mmmm()
+{
+ //:: ExpectedOutput(exhale.failed:qp.not.injective)
+ //:: ExpectedOutput(exhale.failed:insufficient.permission)
+ //:: MissingOutput(exhale.failed:insufficient.permission, /silicon/issue/34/)
+ exhale forall i: Int :: p()
+}
+
+method mmmm2()
+{
+ //:: ExpectedOutput(inhale.failed:qp.not.injective)
+ inhale forall i: Int :: p()
+}
diff --git a/src/test/resources/all/issues/silicon/0595.vpr b/src/test/resources/all/issues/silicon/0595.vpr
@@ -7,7 +7,6 @@ predicate P()
 
 method test()
   requires P()
-   //:: IgnoreFile(/carbon/issue/391/)
   ensures forall i: Int :: i == 0 ==> P()
 {}