Chalice: Two new test-cases for recently fixed problems.

4 files changed, 44 insertions, 0 deletions

diff --git a/Chalice/tests/general-tests/FunctionPostcondition.chalice b/Chalice/tests/general-tests/FunctionPostcondition.chalice
new file mode 100644
index 00000000..7fd95b05
--- /dev/null
+++ b/Chalice/tests/general-tests/FunctionPostcondition.chalice
@@ -0,0 +1,10 @@
+// this test is for function postconditions

+

+class FunctionPostconditions

+{

+  predicate valid { true }

+  

+  function t1(): int

+    ensures unfolding valid in true;

+  { 1 }

+}

diff --git a/Chalice/tests/general-tests/FunctionPostcondition.output.txt b/Chalice/tests/general-tests/FunctionPostcondition.output.txt
new file mode 100644
index 00000000..3244dc57
--- /dev/null
+++ b/Chalice/tests/general-tests/FunctionPostcondition.output.txt
@@ -0,0 +1,4 @@
+Verification of FunctionPostcondition.chalice using parameters="" 

+

+The program did not typecheck.

+8.5: the postcondition of functions cannot contain unfolding expressions at the moment

diff --git a/Chalice/tests/regressions/internal-bug-7.chalice b/Chalice/tests/regressions/internal-bug-7.chalice
new file mode 100644
index 00000000..9f7d474d
--- /dev/null
+++ b/Chalice/tests/regressions/internal-bug-7.chalice
@@ -0,0 +1,26 @@
+class Node {
+  var n: Node
+  
+  predicate P { acc(n) && (n != null ==> acc(n.P)) }
+
+  function length(): int
+    requires rd(P)
+    ensures result >= 1
+  { unfolding rd(P) in 1 + (n == null ? 0 : n.length()) }
+  
+}
+
+class Test {
+  method test(node: Node)
+    requires node != null
+    requires acc(node.P)
+  {
+    assert node.length() >= 1
+    assert (unfolding rd(node.P) in node.n == null) ==> (node.length() == 1) /* Holds in Chalice and Syxc */
+    //assert (unfolding rd(node.P) in node.n != null) ==> (unfolding rd(node.P) in node.n.length() >= 1) /* Holds in Chalice and Syxc */
+    assert (unfolding rd(node.P) in node.n != null) ==> (node.length() > 1) /* Holds in Chalice and Syxc */
+    assert (node.length() == 1) ==> (unfolding rd(node.P) in node.n == null) /* Fails in Chalice and Syxc */
+    assert (node.length() == 1) <==> (unfolding rd(node.P) in node.n == null)
+    // assert n.length() > 1 <==> unfolding rd(n.P) in n.n != null /* Fails in Chalice and Syxc */
+  }
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/internal-bug-7.output.txt b/Chalice/tests/regressions/internal-bug-7.output.txt
new file mode 100644
index 00000000..78ae95fd
--- /dev/null
+++ b/Chalice/tests/regressions/internal-bug-7.output.txt
@@ -0,0 +1,4 @@
+Verification of internal-bug-7.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings