1 files changed, 109 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/test7.chalice b/Chalice/tests/predicates/test7.chalice
new file mode 100644
index 00000000..6ad8e592
--- /dev/null
+++ b/Chalice/tests/predicates/test7.chalice
@@ -0,0 +1,109 @@
+class C
+{
+  var value:int;
+  
+  predicate inv { acc(value) }
+  
+  function get():int
+    requires inv;
+  {
+    unfolding inv in value
+  }
+  
+  method set(newval:int)
+    requires inv;
+    ensures inv && get()==newval;
+  {
+    unfold inv;
+    value:=newval;
+    fold inv;
+  }
+  
+  method callmethod0()
+    requires inv;
+    ensures inv && get()==3;
+  {
+    call set(3);
+  }
+  
+  method callmethod1()
+  {
+    call set(3); // ERROR: should fail
+  }
+  
+  method ifc()
+    requires inv;
+    ensures inv && get()>old(get())
+  {
+    if(get()>0) { call set(get()+get()); }
+    else { call set(2); }
+  }
+  
+  method loop0() returns (r:int)
+    requires inv && get()>0;
+    ensures inv && r==get();
+  {
+    r:=0;
+    while (r<unfolding inv in value)
+      invariant inv && r<=get();
+    { r:=r+1; }
+  }
+  
+  method loop1() returns (r:int)
+    requires inv && get()>0;
+    ensures inv && r==get();
+  {
+    r:=0;
+    while (r<get())
+      invariant inv && r<=unfolding inv in value;
+    { r:=r+1; }
+  }
+  
+  method uf0()
+    requires acc(value);
+  {
+    assert acc(value);
+    fold inv;
+    assert acc(value); // ERROR: should fail
+  }
+  
+  method uf1()
+    requires acc(value);
+  {
+    assert acc(value);
+    fold inv;
+    assert acc(inv);
+  }
+  
+  method uf2()
+    requires inv;
+  {
+    assert inv;
+    unfold inv;
+    assert acc(value);
+  }
+  
+  method uf3()
+    requires inv;
+  {
+    assert inv;
+    unfold inv;
+    assert acc(inv); // ERROR: should fail
+  }
+  
+  method badframing0()
+    requires get()==2;  // ERROR: should fail
+  {}
+  
+  method badframing1()
+    requires value==2; // ERROR: should fail
+  {}
+  
+  method badframing2()
+    requires acc(value) && get()==2;  // ERROR: should fail
+  {}
+  
+  method badframing3()
+    requires inv && value==2; // ERROR: should fail
+  {}
+}
+\ No newline at end of file