diff options
| author |  stefanheule <unknown> | 2011-07-07 17:44:52 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-07 17:44:52 +0200 |
| commit | 2c3e6b564ac92f7b4cd53779406b5c1359832792 (patch) | |
| tree | d37c4564eb742b26415becdd953828d70d16db29 /Chalice/tests/permission-model | |
| parent | c1f5342aac7c1d95c5f3281726e2cfd00051001e (diff) | |
Chalice: Error message of the valid-permission-check often included '<undefined position>'. Reference output of one affected test updated.
Diffstat (limited to 'Chalice/tests/permission-model')
| -rw-r--r-- | Chalice/tests/permission-model/permission_arithmetic.output.txt | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt index afbd9be7..0b2b5335 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -1,13 +1,13 @@ Verification of permission_arithmetic.chalice using parameters=""
- 24.5: Assertion might not hold. The permission at 24.18 might not be positive.
- 40.5: The precondition at 33.14 might not hold. The permission at 33.20 might not be positive.
+ 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.19 might not be positive.
+ 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.
Boogie program verifier finished with 47 verified, 9 errors
|