blob: b9d20e0805670829c728dd4cba3ddb91002de153 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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
|
