blob: c6c5fe0e94d1f0cdfbaa98d741da5a5cb8b67ff7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Verification of prog1.chalice using parameters=""
9.10: Location might not be readable.
25.5: Location might not be writable
33.14: Location might not be readable.
42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
60.5: Location might not be writable
76.5: The target of the unshare statement might not be shared.
84.5: The target of the unshare statement might not be shared.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
7.3: The end of method seq0 is unreachable.
21.3: The end of method seq3 is unreachable.
28.3: The end of method main0 is unreachable.
53.3: The end of method main3 is unreachable.
73.3: The end of method main5 is unreachable.
78.3: The end of method main6 is unreachable.
Boogie program verifier finished with 7 errors and 6 smoke test warnings
|
