Chalice: New test case for predicates.

1 files changed, 38 insertions, 0 deletions

diff --git a/Chalice/tests/predicates/test.chalice b/Chalice/tests/predicates/test.chalice
new file mode 100644
index 00000000..6c416671
--- /dev/null
+++ b/Chalice/tests/predicates/test.chalice
@@ -0,0 +1,38 @@
+class List

+{

+  var value:int;

+  var next:List;

+  

+  predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }

+  

+  function len():int

+    requires inv;

+  {

+    unfolding inv in (next==null) ? 1 : (1+next.len())

+  }

+  

+  predicate P { acc(value,50) }

+  

+  method skip()

+    requires P; ensures P

+  {}

+  

+  method goo()

+    requires acc(value);

+  {

+    // mask: value=100, secmask: -

+    fold P;

+    // mask: value=50,p=100, secmask: value=50

+    call skip();

+    // mask: value=50,p=100, secmask: -

+    fold P;

+    // mask: value=0,p=200, secmask: value=50

+    fork t:=skip();

+    // mask: value=0,p=100, secmask: -

+    assert unfolding P in value==old(value);

+    // ERROR: Chalice currently cannot verify this example, as there is neither

+    // primary nor secondary permission available to value directly before the

+    // assertion

+  }

+

+}