diff options
| author |  stefanheule <unknown> | 2011-07-18 11:50:29 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-18 11:50:29 +0200 |
| commit | 186b3e2e4a8b461212f9b97255b5f64d045df23f (patch) | |
| tree | 0f4b495540d05df739c2e684f14831f4e3f66528 /Chalice/tests | |
| parent | e8272220e94c52a8425cba727bebb5f7050405ab (diff) | |
Chalice: Also exhale correctly in two steps for multiple contracts (e.g. two preconditions), and include missing well-formedness assumption afer async method calls.
Diffstat (limited to 'Chalice/tests')
| -rw-r--r-- | Chalice/tests/permission-model/permission_arithmetic.chalice | 15 | ||||
| -rw-r--r-- | Chalice/tests/permission-model/permission_arithmetic.output.txt | 3 |
2 files changed, 17 insertions, 1 deletions
diff --git a/Chalice/tests/permission-model/permission_arithmetic.chalice b/Chalice/tests/permission-model/permission_arithmetic.chalice index fa457981..0cdf8aae 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.chalice +++ b/Chalice/tests/permission-model/permission_arithmetic.chalice @@ -205,6 +205,21 @@ class Cell { 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)
{ }
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt index f4859de5..277b5da6 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -10,5 +10,6 @@ Verification of permission_arithmetic.chalice using parameters="" 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.
-Boogie program verifier finished with 58 verified, 10 errors
+Boogie program verifier finished with 61 verified, 11 errors
|