blob: 98cd0d4e9f3f6712f827eede9dd19a6cad722b6b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
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.
Boogie program verifier finished with 20 verified, 10 errors
|
