diff options
Diffstat (limited to 'Chalice/tests/permission-model')
31 files changed, 0 insertions, 1237 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);
- {
- }
-
-}
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt deleted file mode 100644 index b2bf49bd..00000000 --- a/Chalice/tests/permission-model/basic.output.txt +++ /dev/null @@ -1,8 +0,0 @@ -Verification of basic.chalice using parameters=""
-
- 28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x. - 48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x. - 97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x. - 148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x. - -Boogie program verifier finished with 4 errors and 0 smoke test warnings
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);
diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt deleted file mode 100644 index b2f76ab6..00000000 --- a/Chalice/tests/permission-model/channels.output.txt +++ /dev/null @@ -1,6 +0,0 @@ -Verification of channels.chalice using parameters=""
-
- 8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f. - 18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f. - -Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/generate_reference.bat b/Chalice/tests/permission-model/generate_reference.bat deleted file mode 100644 index c9b04fcd..00000000 --- a/Chalice/tests/permission-model/generate_reference.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%~nx0" %*
diff --git a/Chalice/tests/permission-model/generate_reference_all.bat b/Chalice/tests/permission-model/generate_reference_all.bat deleted file mode 100644 index c9b04fcd..00000000 --- a/Chalice/tests/permission-model/generate_reference_all.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%~nx0" %*
diff --git a/Chalice/tests/permission-model/locks.chalice b/Chalice/tests/permission-model/locks.chalice deleted file mode 100644 index 5107fd38..00000000 --- a/Chalice/tests/permission-model/locks.chalice +++ /dev/null @@ -1,146 +0,0 @@ -class Cell {
- var x: int;
-
- // use starred read permission
- invariant rd*(x);
-
- method a1(c: Cell)
- requires c != null && rd(c.mu) && waitlevel << c;
- {
- acquire c;
- assert(rd*(c.x));
-
- release c;
- assert(rd*(c.x));
- }
-
- method a2(c: Cell)
- requires c != null && rd(c.mu) && waitlevel << c;
- {
- acquire c;
- assert(rd(c.x)); // ERROR: should fail
-
- release c;
- assert(rd(c.x)); // ERROR: should fail
- }
-
- method a3()
- {
- var c: Cell := new Cell;
-
- share c;
- assert(rd*(c.x));
-
- acquire c;
- unshare c;
- assert(rd*(c.x));
- }
-
- method a4()
- {
- var c: Cell := new Cell;
-
- share c;
- assert(rd(c.x)); // ERROR: should fail
- }
-
- method a5()
- {
- var c: Cell := new Cell;
-
- share c;
- acquire c;
- unshare c;
- assert(rd(c.x)); // ERROR: should fail
- }
-
-}
-
-
-class Cell2 {
- var x: int;
-
- // use normal fractional permission
- invariant rd(x);
-
- method a1(c: Cell2)
- requires c != null && rd(c.mu) && waitlevel << c;
- {
- acquire c;
- assert(rd*(c.x));
-
- release c;
- assert(rd*(c.x)); // ERROR: we gave away all permission
- }
-
- method a2(c: Cell2)
- requires c != null && rd(c.mu) && waitlevel << c;
- {
- acquire c;
- assert(rd(c.x)); // ERROR: should fail
-
- release c;
- assert(rd(c.x)); // ERROR: should fail
- }
-
- method a3()
- {
- var c: Cell2 := new Cell2;
-
- share c;
- assert(rd*(c.x));
-
- call void(c);
- assert(rd*(c.x));
-
- call dispose(c);
- assert(rd*(c.x));
-
- acquire c;
- unshare c;
- assert(rd*(c.x));
-
- assert(acc(c.x)); // ERROR: should fail
- }
-
- method a4(c: Cell2)
- requires c != null && acc(c.mu) && holds(c);
- requires rd(c.x);
- lockchange c
- {
- release c; // ERROR: should fail, we don't have enough permission
- }
-
- method a5()
- {
- var c: Cell2 := new Cell2;
-
- share c;
- acquire c;
- assert(acc(c.x));
-
- unshare c;
- assert(acc(c.x));
- }
-
- method a6(c: Cell2)
- requires acc(c.x,rd(c)) && acc(c.mu) && c.mu == lockbottom
- {
- var n: int;
-
- share c;
- rd acquire c;
- n := c.x
- rd release c;
-
- n := c.x // ERROR: no read access possible
-
- acquire c;
- unshare c;
- }
-
- method void(c: Cell2) requires rd(c.x); ensures rd(c.x); {}
-
- method dispose(c: Cell2) requires rd(c.x); {}
-
-}
diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt deleted file mode 100644 index 6b3a7abe..00000000 --- a/Chalice/tests/permission-model/locks.output.txt +++ /dev/null @@ -1,20 +0,0 @@ -Verification of locks.chalice using parameters=""
-
- 21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x. - 24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x. - 44.5: Assertion might not hold. Insufficient fraction at 44.12 for Cell.x. - 54.5: Assertion might not hold. Insufficient fraction at 54.12 for Cell.x. - 73.5: Assertion might not hold. Insufficient fraction at 73.12 for Cell2.x. - 80.5: Assertion might not hold. Insufficient fraction at 80.12 for Cell2.x. - 83.5: Assertion might not hold. Insufficient fraction at 83.12 for Cell2.x. - 103.5: Assertion might not hold. Insufficient fraction at 103.12 for Cell2.x. - 111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x. - 136.10: Location might not be readable. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 66.3: The end of method a1 is unreachable. - 76.3: The end of method a2 is unreachable. - 86.3: The end of method a3 is unreachable. - 138.5: The statements after the acquire statement are unreachable. - -Boogie program verifier finished with 10 errors and 4 smoke test warnings
diff --git a/Chalice/tests/permission-model/peculiar.chalice b/Chalice/tests/permission-model/peculiar.chalice deleted file mode 100644 index 31c4d259..00000000 --- a/Chalice/tests/permission-model/peculiar.chalice +++ /dev/null @@ -1,55 +0,0 @@ -class Cell {
- var x: int;
-
- invariant rd(x);
-
- method t1()
- requires acc(x);
- ensures rd(x) && rd(x);
- {
- }
-
- method t2()
- requires acc(x,1);
- ensures rd(x);
- {
- call void();
- }
-
- method t3()
- requires rd(x);
- {
- call t3helper();
- }
-
- method t3helper()
- requires rd(x) && rd(x);
- ensures rd(x) && rd(x);
- {}
-
- method t4()
- requires rd(x);
- {
- call dispose();
- call void(); // call succeeds, even though the precondition is also rd(x), and the next assertion fails
- assert(rd(x)); // ERROR: fails, as this check is done exactly (as it would in a postcondition)
- }
-
- method t5(n: int)
- requires acc(x);
- {
- var i: int := 0;
- call req99();
- while (i < n)
- invariant rd*(x);
- {
- call dispose();
- i := i+1
- }
- }
-
- method dispose() requires rd(x); {}
- method void() requires rd(x); ensures rd(x); {}
- method req99() requires acc(x,99); {}
-
-}
diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt deleted file mode 100644 index 07104e77..00000000 --- a/Chalice/tests/permission-model/peculiar.output.txt +++ /dev/null @@ -1,8 +0,0 @@ -Verification of peculiar.chalice using parameters=""
-
- 35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 30.3: The end of method t4 is unreachable. - -Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/permission-model/permarith_parser.chalice b/Chalice/tests/permission-model/permarith_parser.chalice deleted file mode 100644 index 5b011d79..00000000 --- a/Chalice/tests/permission-model/permarith_parser.chalice +++ /dev/null @@ -1,37 +0,0 @@ -class Cell {
- var x: int;
- var y: Cell;
-
- method a1()
- requires acc(x,y); // ERROR: amount is not integer
- {
- }
-
- method a2()
- requires acc(x,n); // ERROR: unknown variable
- {
- }
-
- method a3()
- requires acc(x,rd(rd(1))); // ERROR: invalid permission expression
- {
- }
-
- method a4()
- requires acc(x,rd*(y)); // ERROR: invalid permission expression
- {
- }
-
- method a5()
- requires acc(x,rd(this.mu)); // ERROR: invalid type inside rd
- requires acc(x,rd(null)); // ERROR: invalid type inside rd
- requires acc(x,rd(true)); // ERROR: invalid type inside rd
- {
- }
-
- method a6()
- requires acc(x,rd(x)*rd(x)); // ERROR: permission multiplication not allowed
- {
- }
-
-}
diff --git a/Chalice/tests/permission-model/permarith_parser.output.txt b/Chalice/tests/permission-model/permarith_parser.output.txt deleted file mode 100644 index bc6598a1..00000000 --- a/Chalice/tests/permission-model/permarith_parser.output.txt +++ /dev/null @@ -1,13 +0,0 @@ -Verification of permarith_parser.chalice using parameters=""
-
-The program did not typecheck.
-6.14: fraction in permission must be of type integer
-11.20: undeclared member n in class Cell
-16.26: permission not expected here.
-16.26: type $Permission is not supported inside a rd expression.
-21.20: rd expression is allowed only in positive predicate contexts
-21.14: expression of type bool invalid in permission
-26.20: type $Mu of variable mu is not supported inside a rd expression.
-27.23: type null is not supported inside a rd expression.
-28.23: type bool is not supported inside a rd expression.
-33.14: multiplication of permission amounts not supported
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); {}
-}
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt deleted file mode 100644 index b9d20e08..00000000 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ /dev/null @@ -1,22 +0,0 @@ -Verification of permission_arithmetic.chalice using parameters=""
-
- 26.5: Assertion might not hold. The permission at 26.12 might not be positive. - 42.5: The precondition at 35.14 might not hold. The permission at 35.14 might not be positive. - 75.3: The postcondition at 77.13 might not hold. Insufficient fraction at 77.13 for Cell.x. - 88.3: The postcondition at 90.13 might not hold. Insufficient epsilons at 90.22 for Cell.x. - 105.20: Location might not be readable. - 111.20: Location might not be readable. - 147.5: Monitor invariant might not hold. Insufficient fraction at 8.13 for Cell.x. - 164.3: The postcondition at 166.13 might not hold. The permission at 166.13 might not be positive. - 176.3: The postcondition at 178.13 might not hold. Insufficient fraction at 178.13 for Cell.x. - 205.10: Location might not be readable. - 220.10: Location might not be readable. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 18.3: Precondition of method a2 is equivalent to false. - 24.3: The end of method a3 is unreachable. - 42.5: The statements after the method call statement are unreachable. - 200.3: The end of method a28 is unreachable. - 215.3: The end of method a28b is unreachable. - -Boogie program verifier finished with 11 errors and 5 smoke test warnings
diff --git a/Chalice/tests/permission-model/predicate_error1.chalice b/Chalice/tests/permission-model/predicate_error1.chalice deleted file mode 100644 index 0726e349..00000000 --- a/Chalice/tests/permission-model/predicate_error1.chalice +++ /dev/null @@ -1,20 +0,0 @@ -class Cell {
- var x: int;
-
- // --- some predicates ---
-
- predicate write1 { acc(x) } // full permission in a predicate
- predicate write2 { acc(x,10) } // 10%
- predicate read1 { rd(x) } // fractional read permission
- predicate read2 { rd*(x) } // starred fractional read permission
- predicate read3 { rd(x,1) } // counting permission (1 epsilon)
-
- // --- invalid permission scaling ---
-
- method error()
- requires rd(read3);
- {
- unfold rd(read3); // ERROR: scaling epsilons is not possible
- }
-
-}
diff --git a/Chalice/tests/permission-model/predicate_error1.output.txt b/Chalice/tests/permission-model/predicate_error1.output.txt deleted file mode 100644 index a5e27bac..00000000 --- a/Chalice/tests/permission-model/predicate_error1.output.txt +++ /dev/null @@ -1,3 +0,0 @@ -Verification of predicate_error1.chalice using parameters=""
-
-Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error2.chalice b/Chalice/tests/permission-model/predicate_error2.chalice deleted file mode 100644 index cc8d7d28..00000000 --- a/Chalice/tests/permission-model/predicate_error2.chalice +++ /dev/null @@ -1,20 +0,0 @@ -class Cell {
- var x: int;
-
- // --- some predicates ---
-
- predicate write1 { acc(x) } // full permission in a predicate
- predicate write2 { acc(x,10) } // 10%
- predicate read1 { rd(x) } // fractional read permission
- predicate read2 { rd*(x) } // starred fractional read permission
- predicate read3 { rd(x,1) } // counting permission (1 epsilon)
-
- // --- invalid permission scaling ---
-
- method error()
- requires rd(read1,1);
- {
- unfold rd(read1,1); // ERROR: scaling epsilons is not possible
- }
-
-}
diff --git a/Chalice/tests/permission-model/predicate_error2.output.txt b/Chalice/tests/permission-model/predicate_error2.output.txt deleted file mode 100644 index fb660013..00000000 --- a/Chalice/tests/permission-model/predicate_error2.output.txt +++ /dev/null @@ -1,3 +0,0 @@ -Verification of predicate_error2.chalice using parameters=""
-
-Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error3.chalice b/Chalice/tests/permission-model/predicate_error3.chalice deleted file mode 100644 index eb1d8777..00000000 --- a/Chalice/tests/permission-model/predicate_error3.chalice +++ /dev/null @@ -1,20 +0,0 @@ -class Cell {
- var x: int;
-
- // --- some predicates ---
-
- predicate write1 { acc(x) } // full permission in a predicate
- predicate write2 { acc(x,10) } // 10%
- predicate read1 { rd(x) } // fractional read permission
- predicate read2 { rd*(x) } // starred fractional read permission
- predicate read3 { rd(x,1) } // counting permission (1 epsilon)
-
- // --- invalid permission scaling ---
-
- method error()
- requires rd(read3,1);
- {
- unfold rd(read3,1); // ERROR: scaling epsilons is not possible
- }
-
-}
diff --git a/Chalice/tests/permission-model/predicate_error3.output.txt b/Chalice/tests/permission-model/predicate_error3.output.txt deleted file mode 100644 index 9f5b503c..00000000 --- a/Chalice/tests/permission-model/predicate_error3.output.txt +++ /dev/null @@ -1,3 +0,0 @@ -Verification of predicate_error3.chalice using parameters=""
-
-Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error4.chalice b/Chalice/tests/permission-model/predicate_error4.chalice deleted file mode 100644 index 0726e349..00000000 --- a/Chalice/tests/permission-model/predicate_error4.chalice +++ /dev/null @@ -1,20 +0,0 @@ -class Cell {
- var x: int;
-
- // --- some predicates ---
-
- predicate write1 { acc(x) } // full permission in a predicate
- predicate write2 { acc(x,10) } // 10%
- predicate read1 { rd(x) } // fractional read permission
- predicate read2 { rd*(x) } // starred fractional read permission
- predicate read3 { rd(x,1) } // counting permission (1 epsilon)
-
- // --- invalid permission scaling ---
-
- method error()
- requires rd(read3);
- {
- unfold rd(read3); // ERROR: scaling epsilons is not possible
- }
-
-}
diff --git a/Chalice/tests/permission-model/predicate_error4.output.txt b/Chalice/tests/permission-model/predicate_error4.output.txt deleted file mode 100644 index 16da656f..00000000 --- a/Chalice/tests/permission-model/predicate_error4.output.txt +++ /dev/null @@ -1,3 +0,0 @@ -Verification of predicate_error4.chalice using parameters=""
-
-Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicates.chalice b/Chalice/tests/permission-model/predicates.chalice deleted file mode 100644 index 1f752fda..00000000 --- a/Chalice/tests/permission-model/predicates.chalice +++ /dev/null @@ -1,103 +0,0 @@ -class Cell {
- var x: int;
-
- // --- some predicates ---
-
- predicate write1 { acc(x) } // full permission in a predicate
- predicate write2 { acc(x,10) } // 10%
- predicate read1 { rd(x) } // fractional read permission
- predicate read2 { rd*(x) } // starred fractional read permission
- predicate read3 { rd(x,1) } // counting permission (1 epsilon)
-
- // --- basic tests ---
-
- method b1()
- requires write1 && write2 && read1 && read2 && read3;
- ensures write1 && write2 && read1 && read2 && read3;
- {
- }
-
- method b2()
- requires write1;
- ensures read1;
- {
- unfold write1;
- fold read1;
- }
-
- method b3()
- requires read1;
- ensures read3;
- {
- unfold read1;
- fold read3;
- fold read2;
- fold read3;
- fold read2;
- fold write1; // ERROR: should fail
- }
-
- method b4()
- requires read2;
- ensures read2;
- {
- unfold read2;
- call dispose();
- fold read2;
- }
-
- method b5()
- requires read1;
- ensures read1;
- {
- unfold read1;
- call dispose();
- fold read1; // ERROR: should fail
- }
-
- method b6()
- requires acc(x);
- ensures acc(x);
- {
- fold read1;
- unfold read1;
- }
-
- method b7() // ERROR: precondition does not hold
- requires acc(x);
- ensures acc(x);
- {
- fold read2;
- unfold read2;
- }
-
- method b8()
- requires acc(x);
- ensures acc(x);
- {
- fold read3;
- unfold read3;
- }
-
- method b9()
- requires acc(x);
- ensures acc(x);
- {
- fold write1;
- unfold write1;
- }
-
- method b10()
- requires acc(x);
- ensures acc(x);
- {
- fold write2;
- unfold write2;
- }
-
- // --- helper functions ---
-
- method void() requires rd(x); ensures rd(x); {}
- method dispose() requires rd(x); {}
-
-}
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt deleted file mode 100644 index 2f4acf7b..00000000 --- a/Chalice/tests/permission-model/predicates.output.txt +++ /dev/null @@ -1,11 +0,0 @@ -Verification of predicates.chalice using parameters=""
-
- 37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x. - 55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x. - 66.3: The postcondition at 68.13 might not hold. Insufficient fraction at 68.13 for Cell.x. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 28.3: The end of method b3 is unreachable. - 49.3: The end of method b5 is unreachable. - -Boogie program verifier finished with 3 errors and 2 smoke test warnings
diff --git a/Chalice/tests/permission-model/reg_test.bat b/Chalice/tests/permission-model/reg_test.bat deleted file mode 100644 index c9b04fcd..00000000 --- a/Chalice/tests/permission-model/reg_test.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%~nx0" %*
diff --git a/Chalice/tests/permission-model/reg_test_all.bat b/Chalice/tests/permission-model/reg_test_all.bat deleted file mode 100644 index c9b04fcd..00000000 --- a/Chalice/tests/permission-model/reg_test_all.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%~nx0" %*
diff --git a/Chalice/tests/permission-model/scaling.chalice b/Chalice/tests/permission-model/scaling.chalice deleted file mode 100644 index ffe9aac1..00000000 --- a/Chalice/tests/permission-model/scaling.chalice +++ /dev/null @@ -1,76 +0,0 @@ -
-class Cell {
- var x: int;
-
- // --- some predicates ---
-
- predicate write1 { acc(x) } // full permission in a predicate
- predicate write2 { acc(x,10) } // 10%
- predicate read1 { rd(x) } // abstract read permission
- predicate read2 { rd*(x) } // starred read permission
- predicate read3 { rd(x,1) } // counting permission (1 epsilon)
-
- // --- permission scaling ---
-
- method s1()
- requires rd(read1);
- {
- unfold rd(read1);
- assert(rd*(x));
- assert(rd(x)); // ERROR: should fail
- }
-
- method s2() // INCOMPLETNESS: postcondition should hold, but fails at the moment
- requires rd(read1);
- ensures rd(read1);
- {
- unfold rd(read1);
- fold rd(read1);
- }
-
- method s3()
- requires acc(x);
- ensures rd(read1);
- {
- fold rd(read1);
- assert(rd*(x));
- assert(acc(x)); // ERROR: should fail
- }
-
- method s4() // ERROR: postcondition does not hold
- requires acc(x);
- ensures read1;
- {
- fold rd(read1);
- }
-
- method s5()
- requires rd(read2);
- {
- unfold rd(read2);
- assert(rd*(x));
- assert(rd(x)); // ERROR: should fail
- }
-
- method s6()
- requires acc(x);
- ensures rd(read2);
- {
- fold rd(read2);
- assert(rd*(x));
- assert(acc(x)); // ERROR: should fail
- }
-
- method s7() // ERROR: postcondition does not hold
- requires acc(x);
- ensures read2;
- {
- fold rd(read2);
- }
-
- // --- helper functions ---
-
- method void() requires rd(x); ensures rd(x); {}
- method dispose() requires rd(x); {}
-
-}
diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt deleted file mode 100644 index 2ba1640a..00000000 --- a/Chalice/tests/permission-model/scaling.output.txt +++ /dev/null @@ -1,16 +0,0 @@ -Verification of scaling.chalice using parameters=""
-
- 20.5: Assertion might not hold. Insufficient fraction at 20.12 for Cell.x. - 23.3: The postcondition at 25.13 might not hold. Insufficient fraction at 25.13 for Cell.read1. - 37.5: Assertion might not hold. Insufficient fraction at 37.12 for Cell.x. - 40.3: The postcondition at 42.13 might not hold. Insufficient fraction at 42.13 for Cell.read1. - 52.5: Assertion might not hold. Insufficient fraction at 52.12 for Cell.x. - 61.5: Assertion might not hold. Insufficient fraction at 61.12 for Cell.x. - 64.3: The postcondition at 66.13 might not hold. Insufficient fraction at 66.13 for Cell.read2. - -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 15.3: The end of method s1 is unreachable. - 31.3: The end of method s3 is unreachable. - 55.3: The end of method s6 is unreachable. - -Boogie program verifier finished with 7 errors and 3 smoke test warnings
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;
-}
diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt deleted file mode 100644 index 7c295c9d..00000000 --- a/Chalice/tests/permission-model/sequences.output.txt +++ /dev/null @@ -1,6 +0,0 @@ -Verification of sequences.chalice using parameters=""
-
- 36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f - 60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f - -Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/test.bat b/Chalice/tests/permission-model/test.bat deleted file mode 100644 index c9b04fcd..00000000 --- a/Chalice/tests/permission-model/test.bat +++ /dev/null @@ -1,2 +0,0 @@ -@echo off
-call "..\test-scripts\%~nx0" %*
|