blob: 53bcd98d8531bc2a9bba17b511407e486ec8f65c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Verification of counter.chalice using parameters=""
70.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.
81.5: Assertion might not hold. The expression at 81.12 might not evaluate to true.
120.5: The target of the release statement might not be locked by the current thread.
129.7: The mu field of the target of the acquire statement might not be above waitlevel.
137.7: The mu field of the target of the acquire statement might not be above waitlevel.
146.5: The target of the release statement might not be locked by the current thread.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
63.3: The end of method main4 is unreachable.
117.3: The end of method nestedBad0 is unreachable.
129.7: The statements after the acquire statement are unreachable.
137.7: The begging of the lock-block is unreachable.
142.3: The end of method nestedBad3 is unreachable.
Boogie program verifier finished with 6 errors and 5 smoke test warnings
|
