diff options
Diffstat (limited to 'Chalice/tests/permission-model/basic.chalice')
| -rw-r--r-- | Chalice/tests/permission-model/basic.chalice | 232 |
1 files changed, 0 insertions, 232 deletions
diff --git a/Chalice/tests/permission-model/basic.chalice b/Chalice/tests/permission-model/basic.chalice deleted file mode 100644 index 53443a49..00000000 --- a/Chalice/tests/permission-model/basic.chalice +++ /dev/null @@ -1,232 +0,0 @@ -class Cell {
- var x: int;
-
- // dispose a read permission to x
- method dispose_rd()
- requires rd(x);
- ensures true;
- {
- }
-
- // return read permission
- method void()
- requires rd(x);
- ensures rd(x);
- {
- }
-
- // multiple calls to method that destroys rd(x)
- method a1()
- requires rd(x);
- ensures true;
- {
- call dispose_rd();
- call dispose_rd();
- }
-
- // call to method that destroys rd(x) really removes permission
- method a2()
- requires rd(x);
- ensures rd(x);
- {
- call dispose_rd();
- // ERROR: should fail to verify postcondition
- }
-
- // forking and method calls of dispose_rd
- method a3()
- requires rd(x);
- ensures true;
- {
- fork dispose_rd();
- call dispose_rd();
- fork dispose_rd();
- call dispose_rd();
- }
-
- // forking and method calls of dispose_rd
- method a4()
- requires rd(x);
- ensures rd(x);
- {
- fork dispose_rd();
- // ERROR: should fail to verify postcondition
- }
-
- // forking and method calls of dispose_rd
- method a5()
- requires rd(x);
- ensures rd(x,1);
- {
- fork dispose_rd();
- // OK: giving away an epsilon permission however should work
- }
-
- // forking and method calls of dispose_rd
- method a6()
- requires rd(x);
- ensures rd*(x);
- {
- fork dispose_rd();
- // OK: giving away a 'undefined' read permission however should work
- }
-
- // multiple forks of dispose_rd
- method a7()
- requires rd(x);
- ensures true;
- {
- fork dispose_rd();
- fork dispose_rd();
- fork dispose_rd();
- fork dispose_rd();
- fork dispose_rd();
- fork dispose_rd();
- }
-
- // joining to regain permission
- method a8(a: int)
- requires rd(x);
- ensures rd(x)
- {
- fork tk := void();
- join tk;
- }
-
- // joining to regain permission
- method a9(a: int)
- requires rd(x);
- ensures rd(x)
- {
- fork tk := dispose_rd();
- join tk;
- // ERROR: should fail to verify postcondition
- }
-
- // joining to regain permission
- method a10(a: int)
- requires rd(x);
- ensures a == 3 ==> rd(x)
- {
- fork tk := void();
- if (3 == a) {
- join tk;
- }
- }
-
- // finite loop of method calls, preserving rd(x)
- method a11()
- requires rd(x);
- ensures rd(x);
- {
- var i: int;
- i := 0;
- while (i < 1000)
- invariant rd(x);
- {
- call void();
- i := i+1;
- }
- }
-
- // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
- method a12(a: int)
- requires rd(x);
- ensures rd*(x);
- {
- var i: int;
- i := 0;
- while (i < a)
- invariant rd*(x);
- {
- fork dispose_rd();
- i := i+1;
- }
- }
-
- // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
- method a13(a: int)
- requires rd(x);
- ensures rd(x);
- {
- var i: int;
- i := 0;
- while (i < a)
- invariant rd*(x);
- {
- fork dispose_rd();
- i := i+1;
- }
- // ERROR: should fail to verify postcondition
- }
-
- // calling dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
- method a14()
- requires rd(x);
- ensures true;
- {
- call dispose_rd();
-
- var i: int;
- i := 0;
- while (i < 1000)
- invariant rd*(x);
- {
- call dispose_rd();
- i := i+1;
- }
- }
-
- // return unknown permission
- method a15()
- requires rd(x);
- ensures rd*(x);
- {
- call dispose_rd();
- }
-
- // rd in loop invariant
- method a16()
- requires rd(x);
- ensures rd*(x);
- {
- call dispose_rd();
-
- var i: int;
- i := 0;
- while (i < 1000)
- invariant acc(x,rd);
- {
- call void();
- i := i+1;
- }
- }
-
- // rd in method contracts
- method a17()
- requires acc(x,rd);
- {
- call dispose_rd();
- call a17();
- }
-
- // multiple rd in method contracts
- method a18()
- requires rd(x);
- ensures rd(x)
- {
- call a18a()
- call a18b()
- }
- method a18a()
- requires acc(x,2*rd);
- ensures acc(x,rd+rd);
- {
- }
- method a18b()
- requires acc(x,rd+rd);
- ensures acc(x,rd*2);
- {
- }
-
-}
|