diff options
| author |  stefanheule <unknown> | 2012-02-25 03:21:29 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:21:29 -0800 |
| commit | 8a1562747f54584ba71e13d22f042663f1ab4e4b (patch) | |
| tree | 6f730af568cd24aea849900c41290e51c68da772 /Chalice/tests/examples | |
| parent | e3d32c38830db49571d7508c6ab2d442cd0c6bed (diff) | |
Chalice: update reference output of AssocitationList (to remove bogus fail)
Diffstat (limited to 'Chalice/tests/examples')
| -rw-r--r-- | Chalice/tests/examples/AssociationList.output.txt | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt index 53d6428f..2955a814 100644 --- a/Chalice/tests/examples/AssociationList.output.txt +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -2,9 +2,9 @@ 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. -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 73.9: The begging of the while-body is unreachable. - 73.9: The statements after the while-loop are unreachable. - -Boogie program verifier finished with 2 errors and 2 smoke test warnings.
+Boogie program verifier finished with 6 errors and 0 smoke test warnings.
|