blob: 6b3a7abef49367930b2f9bc32dd241bd2e32e24a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
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.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
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.
138.5: The statements after the acquire statement are unreachable.
Boogie program verifier finished with 10 errors and 4 smoke test warnings
|
