blob: 19e84f93fb8bd2c22d34cda6f2d75c3d6517372e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Verification of LoopLockChange.chalice using parameters=""
10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
35.5: The loop might lock/unlock more than the lockchange clause allows.
65.5: The loop might lock/unlock more than the lockchange clause allows.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
10.5: The begging of the while-body is unreachable.
10.5: The statements after the while-loop are unreachable.
75.5: Assumption introduces a contradiction.
Boogie program verifier finished with 3 errors and 3 smoke test warnings.
|
