blob: 167898fb3bf95df9d2eccbb24d780d2c10b54e5a (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Verification of ProdConsChannel.chalice using parameters=""
47.3: Method body is not allowed to leave any debt.
61.3: Method body is not allowed to leave any debt.
85.20: Location might not be readable.
123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
80.5: The end of the while-loop is unreachable.
Boogie program verifier finished with 4 errors and 1 smoke test warnings.
|
