blob: e7ae56f6cf2747c5da83eb2e461848eb55c468e7 (
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
|
