1 files changed, 0 insertions, 45 deletions
diff --git a/Chalice/tests/permission-model/channels.chalice b/Chalice/tests/permission-model/channels.chalice
deleted file mode 100644
index 6a4961cd..00000000
--- a/Chalice/tests/permission-model/channels.chalice
+++ /dev/null
@@ -1,45 +0,0 @@
-class C {
-  var f: int;
-  
-  method t1(ch: C1)
-    requires ch != null && rd(f);
-    ensures true;
-  {
-    send ch(this) // ERROR
-  }
-  
-  method t2(ch: C1)
-    requires ch != null && acc(f);
-    ensures true;
-  {
-    send ch(this)
-  }
-  
-  method t3(ch: C2)
-    requires ch != null && rd(f);
-    ensures rd(f);
-  {
-    send ch(this)
-    // ERROR: should fail to verify postcondition
-  }
-  
-  method t4(ch: C1, a: C) returns (b: C)
-    requires ch != null && credit(ch, 1) && rd(ch.mu) && waitlevel << ch;
-    ensures rd*(b.f);
-  {
-    receive b := ch
-  }
-  
-  method t5(ch: C1)
-    requires ch != null && acc(f,1);
-    ensures true;
-  {
-    send ch(this)
-    send ch(this)
-    send ch(this)
-  }
-  
-}
-
-channel C1(x: C) where rd(x.f);
-channel C2(x: C) where rd*(x.f);