diff options
| author |  stefanheule <unknown> | 2011-08-04 16:15:49 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-08-04 16:15:49 +0200 |
| commit | 256ef437e9642c889e12fe69ff22ccc73d73722a (patch) | |
| tree | 1db65a7de8b160c8a97ade3fe442914603f5a6ac | |
| parent | 54a80970225df5f061edbcb22412a3eaf46b66e2 (diff) | |
Chalice: Add comment to a broken test-case.
| -rw-r--r-- | Chalice/tests/examples/AssociationList.chalice | 9 | ||||
| -rw-r--r-- | Chalice/tests/examples/AssociationList.output.txt | 8 |
2 files changed, 13 insertions, 4 deletions
diff --git a/Chalice/tests/examples/AssociationList.chalice b/Chalice/tests/examples/AssociationList.chalice index cc3ecfb4..418bcd12 100644 --- a/Chalice/tests/examples/AssociationList.chalice +++ b/Chalice/tests/examples/AssociationList.chalice @@ -1,3 +1,12 @@ +/*
+ Note: This example seems to be completely broken. The failing assertion
+ about locking/unlocking too much causes an inconsistency and all following
+ assertions pass by default.
+ It seems that the specification, in particular the loop invariant in method
+ Add, is wrong. (see also http://boogie.codeplex.com/workitem/10207)
+ -- August 2011, Stefan Heule
+*/
+
class Client {
method Main(d: Data)
requires d != null
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt index bfff3c60..53d6428f 100644 --- a/Chalice/tests/examples/AssociationList.output.txt +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -1,10 +1,10 @@ Verification of AssociationList.chalice using parameters=""
- 19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu. - 64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop. + 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. The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. - 64.9: The begging of the while-body is unreachable. - 64.9: The statements after the while-loop are unreachable. + 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.
|