1 files changed, 0 insertions, 85 deletions
diff --git a/Chalice/tests/permission-model/sequences.chalice b/Chalice/tests/permission-model/sequences.chalice
deleted file mode 100644
index 0560945d..00000000
--- a/Chalice/tests/permission-model/sequences.chalice
+++ /dev/null
@@ -1,85 +0,0 @@
-class Program {
-  var x: int;
-  
-  method a(a: seq<A>)
-    requires |a| > 2;
-    requires rd(a[*].f);
-    requires forall i in [0..|a|-1] :: a[i] != null;
-    requires a[0].f == 1;
-    ensures rd(a[*].f);
-  {
-    assert rd(a[*].f);
-    call b(a);
-  }
-  
-  method b(a: seq<A>)
-    requires |a| > 2;
-    requires rd(a[*].f);
-    requires forall i in [0..|a|-1] :: a[i] != null;
-    requires a[0].f == 1;
-    ensures rd(a[*].f);
-  {
-    assert rd(a[*].f);
-  }
-  
-  method c(a: seq<A>)
-    requires |a| > 2;
-    requires rd(a[*].f);
-    requires forall i in [0..|a|-1] :: a[i] != null;
-    requires a[0].f == 1;
-    ensures rd(a[*].f);
-  {
-    call void(a[1]);
-    call void(a[0]);
-  }
-  
-  method c1(a: seq<A>) // ERROR: should fail to verify postcondition
-    requires |a| > 2;
-    requires rd(a[*].f);
-    requires forall i in [0..|a|-1] :: a[i] != null;
-    requires a[0].f == 1;
-    ensures rd(a[*].f);
-  {
-    call dispose(a[1]);
-  }
-  
-  method d(a: seq<A>)
-    requires |a| > 2;
-    requires rd(a[*].f);
-    requires forall i in [0..|a|-1] :: a[i] != null;
-    requires a[0].f == 1;
-    ensures rd*(a[*].f);
-  {
-    call dispose(a[1]); // we don't give away all the permission, thus verification succeeds
-    
-    var x: int;
-    call x := some_number();
-    call dispose(a[x]); // slighly more interesting, but still clearly ok
-  }
-  
-  method e(a: seq<A>) // ERROR: should fail to verify postcondition
-    requires |a| > 2;
-    requires acc(a[*].f,10);
-    requires forall i in [0..|a|-1] :: a[i] != null;
-    requires a[0].f == 1;
-    ensures rd*(a[*].f);
-  {
-    var x: int;
-    call x := some_number();
-    call dispose2(a[x]);
-  }
-  
-  method some_number() returns (a: int)
-    ensures 0 <= a && a < 3;
-  {
-    a := 1;
-  }
-  
-  method dispose(a: A) requires rd(a.f); {}
-  method dispose2(a: A) requires acc(a.f,10); {}
-  method void(a: A) requires rd(a.f); ensures rd(a.f); {}
-}
-
-class A {
-  var f: int;
-}