blob: 18d05658e9da25f96516e7ae2e1ab8377d8cee3a (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Verification of prog3.chalice using parameters=""
76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.
76.3: Method might lock/unlock more than allowed.
191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14 for ReadSharing.x.
202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13 for ReadSharing.x.
The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
191.5: The statements after the method call statement are unreachable.
Boogie program verifier finished with 4 errors and 1 smoke test warnings.
|
