blob: 4ab057dd707ef0cf538b21eda5191bd5ea393a9a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Verification of prog4.chalice using parameters=""
5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
17.7: The target of the release statement might not be locked by the current thread.
17.7: Release might fail because the current thread might hold the read lock.
30.7: The target of the release statement might not be locked by the current thread.
30.7: Release might fail because the current thread might hold the read lock.
34.5: The target of the release statement might not be locked by the current thread.
34.5: Release might fail because the current thread might hold the read lock.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
2.3: The end of method M is unreachable.
Boogie program verifier finished with 7 errors and 1 smoke test warnings
|
