diff options
| author |  stefanheule <unknown> | 2011-07-18 10:44:12 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-18 10:44:12 +0200 |
| commit | e8272220e94c52a8425cba727bebb5f7050405ab (patch) | |
| tree | 83914d59a3dddbfb2b3b0e6e2e55b11f5b590ebc /Chalice/tests/permission-model | |
| parent | e81ea58e400b47065ced037cd6e156516aabd0ca (diff) | |
Chalice: Fix a problem with permission expressions. Prevsiously, exhaling "acc(o.f,100-rd) && acc(o.f,rd)" resulted in a contradiction. This is now solved by using a two-step exhale (loosely speaking, read permissions and functional properties are exhaled first, and only afterwards all other permissions). Extended testcases appropriately.
Diffstat (limited to 'Chalice/tests/permission-model')
| -rw-r--r-- | Chalice/tests/permission-model/permission_arithmetic.chalice | 38 | ||||
| -rw-r--r-- | Chalice/tests/permission-model/permission_arithmetic.output.txt | 21 |
2 files changed, 49 insertions, 10 deletions
diff --git a/Chalice/tests/permission-model/permission_arithmetic.chalice b/Chalice/tests/permission-model/permission_arithmetic.chalice index 94cf30a3..fa457981 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.chalice +++ b/Chalice/tests/permission-model/permission_arithmetic.chalice @@ -2,6 +2,8 @@ class Cell { var x: int;
var i: int;
var y: Cell;
+ var f: int;
+ var g: int;
invariant rd(x);
@@ -189,5 +191,41 @@ class Cell { 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 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 index 0b2b5335..f4859de5 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -1,13 +1,14 @@ Verification of permission_arithmetic.chalice using parameters=""
- 24.5: Assertion might not hold. The permission at 24.12 might not be positive.
- 40.5: The precondition at 33.14 might not hold. The permission at 33.14 might not be positive.
- 73.3: The postcondition at 75.13 might not hold. Insufficient fraction at 75.13 for Cell.x.
- 86.3: The postcondition at 88.13 might not hold. Insufficient epsilons at 88.22 for Cell.x.
- 103.20: Location might not be readable.
- 109.20: Location might not be readable.
- 145.5: Monitor invariant might not hold. Insufficient fraction at 6.13 for Cell.x.
- 162.3: The postcondition at 164.13 might not hold. The permission at 164.13 might not be positive.
- 174.3: The postcondition at 176.13 might not hold. Insufficient fraction at 176.13 for Cell.x.
+ 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.
-Boogie program verifier finished with 47 verified, 9 errors
+Boogie program verifier finished with 58 verified, 10 errors
|