diff options
Diffstat (limited to 'Chalice/tests/permission-model/permission_arithmetic.output.txt')
| -rw-r--r-- | Chalice/tests/permission-model/permission_arithmetic.output.txt | 22 |
1 files changed, 0 insertions, 22 deletions
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
|