diff options
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.
|