1 files changed, 0 insertions, 246 deletions
diff --git a/Chalice/tests/permission-model/permission_arithmetic.chalice b/Chalice/tests/permission-model/permission_arithmetic.chalice
deleted file mode 100644
index 0cdf8aae..00000000
--- a/Chalice/tests/permission-model/permission_arithmetic.chalice
+++ /dev/null
@@ -1,246 +0,0 @@
-class Cell {
-  var x: int;
-  var i: int;
-  var y: Cell;
-  var f: int;
-  var g: int;
-  
-  invariant rd(x);
-  
-  predicate valid { rd(x) }
-  
-  method a1(n: int) // test various arithmetic operations on permissions
-    requires acc(x,1+1) && acc(x,1) && acc(x,3) && acc(x,1-rd(5-7)+rd(3)) && rd(x) && rd(this.y);
-    ensures acc(x,100-97);
-  {
-  }
-  
-  method a2(n: int)
-    requires acc(x,1-rd(1)-2);
-  {
-    assert false; // this should verify, as the precondition contains an invalid permission
-  }
-  
-  method a3(n: int)
-  {
-    assert acc(x,1-rd(1)-2); // ERROR: invalid (negative) permission
-  }
-  
-  method a4(n: int)
-    requires acc(x,rd(n));
-  {
-  }
-  
-  method a5(n: int)
-    requires acc(x,rd(n)-rd(2));
-  {
-  }
-  
-  method a6()
-    requires acc(x);
-  {
-    call a5(1); // ERROR: n=1 makes the permission in the precondition negative
-  }
-  
-  method a7(c: Cell)
-    requires acc(c.x,100-rd(c));
-    requires c != null && acc(c.mu) && waitlevel << c;
-    ensures acc(c.x);
-  {
-    acquire(c);
-    unshare(c);
-  }
-  
-  method a8()
-    requires acc(x,100-rd(valid)) && valid;
-    ensures acc(x);
-  {
-    unfold valid;
-  }
-  
-  method a9()
-    requires acc(x,rd(valid));
-    ensures valid;
-  {
-    fold valid;
-  }
-  
-  method a10()
-    requires valid;
-    ensures acc(x,rd(valid));
-  {
-    unfold valid;
-  }
-  
-  method a11() // ERROR: postcondition does not hold (not enough permission)
-    requires valid;
-    ensures acc(x);
-  {
-    unfold valid;
-  }
-  
-  method a12()
-    requires rd(this.i) && this.i > 0 && acc(x,rd(this.i));
-    ensures rd(this.i) && this.i > 0 && acc(x,rd(i));
-  {
-  }
-  
-  method a13(i: int) // ERROR: postcondition does not hold
-    requires rd(this.i) && this.i > 0 && i > 0 && acc(x,rd(this.i));
-    ensures i > 0 && acc(x,rd(i));
-  {
-  }
-  
-  method a14()
-    requires acc(y) && this.y == this; // test aliasing
-    requires acc(x,100-rd(y));
-    requires y != null && acc(this.mu) && waitlevel << this;
-    ensures acc(x);
-    lockchange this;
-  {
-    acquire this;
-  }
-  
-  method a15()
-    requires acc(x,rd(this.i)); // ERROR: this.i is not readable
-    ensures acc(x,rd(this.i));
-  {
-  }
-  
-  method a16()
-    requires acc(x,rd(this.y)); // ERROR: this.y is not readable
-    ensures acc(x,rd(this.y));
-  {
-  }
-  
-  method a17(tk: token<Cell.void>)
-    requires acc(x,100-rd(tk)) && acc(tk.joinable) && tk.joinable;
-    requires eval(tk.fork this.void(),true);
-    ensures acc(x);
-  {
-    join tk;
-  }
-  
-  method a18()
-    requires acc(x,rd+rd-rd+10*rd-rd*(5+5))
-    ensures rd(x)
-  {
-    call void();
-  }
-  
-  method a19()
-    requires acc(x)
-    requires acc(this.mu) && lockbottom == this.mu
-    ensures acc(x)
-    lockchange this;
-  {
-    share this;
-    acquire this;
-    unshare this;
-  }
-  
-  method a20()
-    requires rd(x)
-    requires acc(this.mu) && lockbottom == this.mu
-    lockchange this;
-  {
-    share this; // ERROR: not enough permission
-  }
-  
-  method a21()
-    requires acc(x,rd*2)
-    ensures rd(x) && rd(x)
-  {
-    assert acc(x,rd+rd)
-    assert acc(x,(1+1)*rd)
-  }
-  
-  method a22()
-    requires acc(x,1*2*5)
-    ensures acc(x,10)
-  {
-  }
-  
-  method a23(c: Cell) // ERROR: permission in postcondition not positive
-    requires acc(x,rd-rd(c))
-    ensures acc(x,rd(c)-rd)
-  {
-  }
-  
-  method a24()
-    requires rd*(x)
-    requires rd*(x)
-  {
-  }
-  
-  method a25() // ERROR: postcondition does not hold, possibly not enough permission
-    requires rd*(x)
-    ensures acc(x,rd)
-  {
-  }
-  
-  // interaction of monitors and predicates
-  method a26()
-    requires acc(x,rd(this))
-    requires acc(mu) && lockbottom == this.mu
-    ensures valid
-    lockchange this
-  {
-    share this
-    acquire this
-    fold valid
-  }
-  
-  method a27()
-    requires acc(f,100-rd) && acc(f,rd)
-  {
-    assert acc(f) // ok, we have full access
-  }
-  
-  method a28()
-    requires acc(f)
-  {
-    call a27();
-    var x: int
-    x := f // ERROR: no permission left
-  }
-  
-  method a27b()
-    requires acc(f,100-rd)
-    requires acc(f,rd)
-  {
-    assert acc(f) // ok, we have full access
-  }
-  
-  method a28b()
-    requires acc(f)
-  {
-    call a27b();
-    var x: int
-    x := f // ERROR: no permission left
-  }
-  
-  method a29()
-    requires acc(f, 100-rd) && acc(g, rd)
-  {  }
-
-  method a30()
-    requires acc(f, 100) && acc(g, rd)
-  {
-    call a29();
-    var tmp: int := this.g;
-  }
-  
-  method a31(c: Cell)
-    requires acc(f, 100-rd) && acc(c.f, rd)
-  {  }
-
-  method a32(c: Cell)
-    requires acc(f, 100) && acc(c.f, rd)
-  {
-    call a31(c);
-    var tmp: int := this.f;
-  }
-  
-  method void() requires rd(x); ensures rd(x); {}
-}