blob: 2955a8144116e0f67628ebdc528a5818f79ac1be (
plain)
1
2
3
4
5
6
7
8
9
10
|
Verification of AssociationList.chalice using parameters=""
28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for mu.
73.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
98.15: Monitor invariant might hot hold. Insufficient fraction at 120.13 for Node.key.
102.15: Monitor invariant might hot hold. Insufficient fraction at 120.13 for Node.key.
73.9: The loop might lock/unlock more than the lockchange clause allows.
107.7: Monitor invariant might hot hold. Insufficient fraction at 120.13 for Node.key.
Boogie program verifier finished with 6 errors and 0 smoke test warnings.
|
