blob: 3492e8079120eede54668bd4a8bf4fddda754f73 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Verification of locks.chalice using parameters=""
21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x.
24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x.
44.5: Assertion might not hold. Insufficient fraction at 44.12 for Cell.x.
54.5: Assertion might not hold. Insufficient fraction at 54.12 for Cell.x.
73.5: Assertion might not hold. Insufficient fraction at 73.12 for Cell2.x.
80.5: Assertion might not hold. Insufficient fraction at 80.12 for Cell2.x.
83.5: Assertion might not hold. Insufficient fraction at 83.12 for Cell2.x.
103.5: Assertion might not hold. Insufficient fraction at 103.12 for Cell2.x.
111.5: Monitor invariant might hot hold. Insufficient fraction at 64.13 for Cell2.x.
136.10: Location might not be readable.
66.3: The end of method a1 is unreachable.
76.3: The end of method a2 is unreachable.
86.3: The end of method a3 is unreachable.
126.3: The end of method a6 is unreachable.
Boogie program verifier finished with 10 errors and 4 smoke test warnings.
|
