diff options
| author |  stefanheule <unknown> | 2011-07-22 16:52:26 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-22 16:52:26 +0200 |
| commit | 2360f6d9b0a7e52f89df8185033e97bb6033df94 (patch) | |
| tree | ded0900004dc57aae235ab38564cca814d2ae779 /Chalice/tests/examples | |
| parent | 3f6a72575ae9c7cee9e26a519cdd1cf2729579d1 (diff) | |
Chalice: Check definedness of where-clause of channels (was missing before), and smoke test for 'false' where clauses. Due to the missing definedness check, a mistake in the specification of CopyLessMessagePassing-with-ack2.chalice was not detected (and has been fixed now).
Diffstat (limited to 'Chalice/tests/examples')
| -rw-r--r-- | Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice | 2 | ||||
| -rw-r--r-- | Chalice/tests/examples/SmokeTestTest.chalice | 1 | ||||
| -rw-r--r-- | Chalice/tests/examples/SmokeTestTest.output.txt | 3 |
3 files changed, 4 insertions, 2 deletions
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice index 77e0018d..3b03853d 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.chalice @@ -13,7 +13,7 @@ channel AckChannel(ch: C) where ch != null && credit(ch, -1); // ack channel C(msg: bool, n: Node, ackC: AckChannel) where
(!msg ==> acc(this.mu, 50) && acc(ackC.mu, 50)) &&
- (msg ==> n != null && acc(n.next) && acc(n.mu) && credit(ackC, -1)); // cell
+ (msg ==> n != null && acc(n.next) && acc(n.mu) && ackC != null && credit(ackC, -1)); // cell
class Node {
var next: Node;
diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice index 44bba5da..6ff283ec 100644 --- a/Chalice/tests/examples/SmokeTestTest.chalice +++ b/Chalice/tests/examples/SmokeTestTest.chalice @@ -118,3 +118,4 @@ class Cell { }
}
+channel C(msg: bool) where msg && !msg // SMOKE: contradiction
\ No newline at end of file diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt index 697119cb..3d1cd786 100644 --- a/Chalice/tests/examples/SmokeTestTest.output.txt +++ b/Chalice/tests/examples/SmokeTestTest.output.txt @@ -18,5 +18,6 @@ The program did not fully verify; the smoke warnings might be misleading if cont 100.5: Assumption introduces a contradiction. 113.5: The statements after the method call statement are unreachable. 116.3: Predicate Cell.valid is equivalent to false. + 121.1: Where clause of channel C is equivalent to false. -Boogie program verifier finished with 1 errors and 15 smoke test warnings.
+Boogie program verifier finished with 1 errors and 16 smoke test warnings.
|