diff options
| author |  Christian Klauser <sealedsun@gmail.com> | 2012-03-27 14:20:18 +0200 |
|---|---|---|
| committer | Christian Klauser <sealedsun@gmail.com> | 2012-03-27 14:20:18 +0200 |
| commit | eb1bb14630dfebb38322ed1841b0cfd50827c122 (patch) | |
| tree | 87f27ba509e3c07aa957daa71b8c5780f8e175a0 /Chalice/tests/examples | |
| parent | 3b45b6e751b6dd8f45a88f1c3ed909f3917f6083 (diff) | |
| parent | 62045c2517dd51f54e40dcfb783fc1370eced93c (diff) | |
Merge
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.
|