blob: 46ac796c57e68c305854f5299569110cc8db20eb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Verification of test7.chalice using parameters=""
31.5: The precondition at 14.14 might not hold. Insufficient fraction at 14.14 for C.inv.
67.5: Assertion might not hold. Insufficient fraction at 67.12 for C.value.
91.5: Assertion might not hold. Insufficient fraction at 91.12 for C.inv.
95.14: Precondition at 8.14 might not hold. Insufficient fraction at 8.14 for C.inv.
99.14: Location might not be readable.
103.28: Precondition at 8.14 might not hold. Insufficient fraction at 8.14 for C.inv.
107.21: 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.
31.5: The statements after the method call statement are unreachable.
62.3: The end of method uf0 is unreachable.
86.3: The end of method uf3 is unreachable.
Boogie program verifier finished with 7 errors and 3 smoke test warnings.
|
