From b25a55b66f8879d83446236ec82973dcd58866c4 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 16 Oct 2009 01:13:00 +0000
Subject: Implicitly declare as local variables undeclared variables occurring
 as LHS's of CALL and RECEIVE statements (as was already done for FORK
 statements).

---
 Chalice/examples/Answer                 | 41 +++++++++++++++---------------
 Chalice/examples/ImplicitLocals.chalice | 27 ++++++++++++++++++++
 Chalice/examples/prog0.chalice          | 44 +++++++++++++++++++++++++++++++++
 3 files changed, 91 insertions(+), 21 deletions(-)
 create mode 100644 Chalice/examples/ImplicitLocals.chalice

(limited to 'Chalice/examples')

diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
index e40b7287..438a9dd6 100644
--- a/Chalice/examples/Answer
+++ b/Chalice/examples/Answer
@@ -1,7 +1,4 @@
 start 
------- Running regression test AssociationList.chalice 
-
-Boogie program verifier finished with 12 verified, 0 errors
 ------ Running regression test cell.chalice 
   142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
 
@@ -152,9 +149,6 @@ The program did not typecheck.
 31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
 32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
 33.19: undeclared member o in class C
-33.10: undefined local variable a
-33.12: undefined local variable b
-33.14: undefined local variable c
 33.5: call of undeclared member m in class int
 34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)
 34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)
@@ -163,8 +157,24 @@ The program did not typecheck.
 58.17: undeclared member sqrt2 in class C
 58.25: undeclared member sqrt2 in class C
 62.17: undeclared member s in class C
-62.10: undefined local variable v
 62.5: call of undeclared member M in class int
+82.5: call of undeclared member MyMethodX in class ImplicitC
+83.12: undefined local variable a
+83.16: undefined local variable b
+83.16: undeclared member k in class int
+88.13: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
+88.13: duplicate actual out-parameter: a
+89.16: undeclared member b in class ImplicitC
+89.16: undeclared member k in class int
+96.21: undeclared member chX in class ImplicitC
+96.5: receive expression (which has type int) does not denote a channel
+97.12: undefined local variable a
+97.16: undefined local variable b
+97.16: undeclared member k in class int
+104.16: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
+104.16: duplicate actual out-parameter: a
+105.16: undeclared member b in class ImplicitC
+105.16: undeclared member k in class int
 ------ Running regression test prog1.chalice 
   9.10: Location might not be readable.
   25.5: Location might not be writable
@@ -195,6 +205,9 @@ Boogie program verifier finished with 51 verified, 4 errors
   27.7: The held field of the target of the release statement might not be writable.
 
 Boogie program verifier finished with 6 verified, 3 errors
+------ Running regression test ImplicitLocals.chalice 
+
+Boogie program verifier finished with 8 verified, 0 errors
 ------ Running regression test RockBand.chalice 
   27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
   41.10: Location might not be readable.
@@ -207,12 +220,6 @@ Boogie program verifier finished with 29 verified, 6 errors
 ------ Running regression test swap.chalice 
 
 Boogie program verifier finished with 5 verified, 0 errors
------- Running regression test GhostConst.chalice 
-The program did not typecheck.
-7.27: undeclared member c in class C
-13.10: ghost variable not allowed here
-21.10: ghost variable not allowed here
-29.10: ghost fields not allowed here
 ------ Running regression test OwickiGries.chalice 
 
 Boogie program verifier finished with 5 verified, 0 errors
@@ -232,11 +239,3 @@ Boogie program verifier finished with 29 verified, 3 errors
 ------ Running regression test RockBand-automagic.chalice 
 
 Boogie program verifier finished with 35 verified, 0 errors
------- Running regression test Leaks.chalice 
-  6.3: Monitor invariant is not allowed to hold write permission to this.mu
-  11.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
-  16.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
-  29.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
-  62.3: Monitor invariant is not allowed to hold write permission to this.mu
-
-Boogie program verifier finished with 7 verified, 5 errors
diff --git a/Chalice/examples/ImplicitLocals.chalice b/Chalice/examples/ImplicitLocals.chalice
new file mode 100644
index 00000000..15ebe8e0
--- /dev/null
+++ b/Chalice/examples/ImplicitLocals.chalice
@@ -0,0 +1,27 @@
+class C {
+  var k: int;
+
+  method MyMethod() returns (x: int, y: C)
+    requires acc(k)
+    ensures acc(y.k) && x < y.k
+  {
+    x := k - 15;
+    y := this;
+  }
+
+  method B() {
+    var c := new C;
+    call a, b := c.MyMethod();
+    assert a < b.k;
+  }
+
+  method D() {
+    var ch := new Ch;
+    var c := new C;
+    send ch(c.k - 15, c);  // give ourselves some credit
+    receive a, b := ch;
+    assert a < b.k;
+  }
+}
+
+channel Ch(x: int, y: C) where acc(y.k) && x < y.k;
diff --git a/Chalice/examples/prog0.chalice b/Chalice/examples/prog0.chalice
index da351c85..7bcb1505 100644
--- a/Chalice/examples/prog0.chalice
+++ b/Chalice/examples/prog0.chalice
@@ -63,3 +63,47 @@ class C {
   }
 }
 class D { }
+
+// ----- tests specifically of implicit locals in CALL and RECEIVE statements
+
+class ImplicitC {
+  var k: int;
+
+  method MyMethod() returns (x: int, y: ImplicitC)
+    requires acc(k)
+    ensures acc(y.k) && x < y.k
+  {
+    x := k - 15;
+    y := this;
+  }
+
+  method B0() {
+    var c := new ImplicitC;
+    call a, b := c.MyMethodX();  // error: method not found (so what is done with a,b?)
+    assert a < b.k;
+  }
+
+  method B1() {
+    var c := new ImplicitC;
+    call a, a := c.MyMethod();  // error: a occurs twice
+    assert a < b.k;
+  }
+
+  method D0() {
+    var ch := new Ch;
+    var c := new ImplicitC;
+    send ch(c.k - 15, c);  // give ourselves some credit
+    receive a, b := chX;  // error: channel not found (so what is done with a,b?)
+    assert a < b.k;
+  }
+
+  method D1() {
+    var ch := new Ch;
+    var c := new ImplicitC;
+    send ch(c.k - 15, c);  // give ourselves some credit
+    receive a, a := ch;  // error: a occurs twice
+    assert a < b.k;
+  }
+}
+
+channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;
-- 
cgit v1.2.3