24 files changed, 1522 insertions, 1515 deletions

diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
index 438a9dd6..d9856d2d 100644
--- a/Chalice/examples/Answer
+++ b/Chalice/examples/Answer
@@ -7,8 +7,8 @@ Boogie program verifier finished with 31 verified, 1 error
   69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.

   80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.

   119.5: The held field of the target of the release statement might not be writable.

-  128.7: The mu field of the target of the acquire statement might not be above maxlock.

-  136.7: The mu field of the target of the acquire statement might not be above maxlock.

+  128.7: The mu field of the target of the acquire statement might not be above waitlevel.

+  136.7: The mu field of the target of the acquire statement might not be above waitlevel.

   145.5: The held field of the target of the release statement might not be writable.

 

 Boogie program verifier finished with 24 verified, 6 errors

diff --git a/Chalice/examples/AssociationList.chalice b/Chalice/examples/AssociationList.chalice
index 6adcbef5..cc3ecfb4 100644
--- a/Chalice/examples/AssociationList.chalice
+++ b/Chalice/examples/AssociationList.chalice
@@ -18,17 +18,17 @@ class AssociationList {
 

   method Init()

     requires acc(head) && acc(mu) && mu == lockbottom

-    ensures acc(mu) && maxlock << this

+    ensures acc(mu) && waitlevel << this

   {

     head := new Node

     head.next := null

     share head

-    share this between maxlock and head

+    share this between waitlevel and head

   }

 

   method Add(key: int, value: Data)

     requires value != null

-    requires rd(mu) && maxlock << this

+    requires rd(mu) && waitlevel << this

     ensures rd(mu)

   {

     acquire this

@@ -46,7 +46,7 @@ class AssociationList {
   }

 

   method Get(key: int) returns (d: Data)

-    requires rd(mu) && maxlock << this

+    requires rd(mu) && waitlevel << this

     ensures rd(mu)

   {

     d := null

@@ -68,8 +68,8 @@ class AssociationList {
           invariant rd(p.next.key) && rd(p.next.value) && acc(p.next.next)

           invariant p.next.next != null ==>

               acc(p.next.next.mu,50) && p.next << p.next.next

-          invariant holds(p) && holds(p.next) && maxlock == p.next.mu

-          invariant p.next.next != null ==> maxlock << p.next.next

+          invariant holds(p) && holds(p.next) && waitlevel == p.next.mu

+          invariant p.next.next != null ==> waitlevel << p.next.next

           lockchange p, p.next.next

         {

           if (p.next.next == null) {

diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice
index 842e3d7d..79e4d75e 100644
--- a/Chalice/examples/CopyLessMessagePassing-with-ack.chalice
+++ b/Chalice/examples/CopyLessMessagePassing-with-ack.chalice
@@ -29,7 +29,7 @@ class Node {
 

 class Program {

   method Putter(e: C, x0: Node) 

-    requires e!= null && acc(e.mu, 50) && e.mu == maxlock && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));

+    requires e!= null && acc(e.mu, 50) && e.mu == waitlevel && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));

   {

     var x: Node := x0;

     var t: Node;

@@ -42,7 +42,7 @@ class Program {
       send e(1, x);

       x := t;

       var ack;

-      assume maxlock << e.mu; // Chalice should be able to figure this out itself

+      assume waitlevel << e.mu; // Chalice should be able to figure this out itself

       receive ack, t := e;

       if(ack != 2) { assume false; /* abort */ }

     }

@@ -50,12 +50,12 @@ class Program {
   }  

   

   method Getter(f: C) 

-    requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.mu;

+    requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu;

   {

     var x: Node := null;

     var msg := 1;

     while(msg != 0)

-      invariant acc(f.mu, 50) && maxlock << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50));

+      invariant acc(f.mu, 50) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50));

     {

       receive msg, x := f;

       if(msg == 0) {

diff --git a/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice b/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice
index 51fd469c..41680258 100644
--- a/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice
+++ b/Chalice/examples/CopyLessMessagePassing-with-ack2.chalice
@@ -32,7 +32,7 @@ class Node {
 

 class Program {

   method Putter(e: C, x0: Node, ackC: AckChannel) 

-    requires e!= null && acc(e.mu, 50) && e.mu == maxlock && acc(ackC.mu, 50) && e.mu << ackC.mu && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));

+    requires e!= null && acc(e.mu, 50) && e.mu == waitlevel && acc(ackC.mu, 50) && e.mu << ackC.mu && (x0 != null ==> x0.list) && (x0 != null ==> credit(e, - 1));

   {

     var x: Node := x0;

     var t: Node;

@@ -45,7 +45,7 @@ class Program {
       send e(1, x, ackC);

       x := t;

       var ack;

-      assume maxlock << ackC.mu; // Chalice should be able to figure this out itself?

+      assume waitlevel << ackC.mu; // Chalice should be able to figure this out itself?

       var ctmp: C;

       receive ctmp := ackC;

       if(ctmp != e) { assume false; /* abort */ }

@@ -54,12 +54,12 @@ class Program {
   }  

   

   method Getter(f: C, ackC: AckChannel) 

-    requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.mu && ackC != null && acc(ackC.mu, 50) && f.mu << ackC.mu;

+    requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu && ackC != null && acc(ackC.mu, 50) && f.mu << ackC.mu;

   {

     var x: Node := null;

     var msg := 1;

     while(msg != 0)

-      invariant acc(f.mu, 50) && maxlock << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50) && acc(ackC.mu, 50));

+      invariant acc(f.mu, 50) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50) && acc(ackC.mu, 50));

     {

       var ackC2: AckChannel;

       receive msg, x, ackC2 := f;

diff --git a/Chalice/examples/CopyLessMessagePassing.chalice b/Chalice/examples/CopyLessMessagePassing.chalice
index 1363bb2a..f5ca2372 100644
--- a/Chalice/examples/CopyLessMessagePassing.chalice
+++ b/Chalice/examples/CopyLessMessagePassing.chalice
@@ -43,12 +43,12 @@ class Program {
   }  

   

   method Getter(f: C) 

-    requires f!= null && credit(f, 1) && acc(f.mu, 50) && maxlock << f.mu;

+    requires f!= null && credit(f, 1) && acc(f.mu, 50) && waitlevel << f.mu;

   {

     var x: Node := null;

     var msg := 1;

     while(msg != 0)

-      invariant acc(f.mu, 50) && maxlock << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50));

+      invariant acc(f.mu, 50) && waitlevel << f.mu && (msg == 1 ==> credit(f, 1)) && (msg == 0 ==> acc(f.mu, 50));

     {

       receive msg, x := f;

       if(msg == 1) {

diff --git a/Chalice/examples/HandOverHand.chalice b/Chalice/examples/HandOverHand.chalice
index f0f6323a..8318a77c 100644
--- a/Chalice/examples/HandOverHand.chalice
+++ b/Chalice/examples/HandOverHand.chalice
@@ -18,7 +18,7 @@ class List {
 

   method Init()

     requires acc(mu) && mu == lockbottom && acc(head) && acc(sum)

-    ensures rd(mu,*) && maxlock << this

+    ensures rd(mu,*) && waitlevel << this

     ensures acc(sum,80) && sum == 0

   {

     var t := new Node

@@ -28,17 +28,17 @@ class List {
     share t

     head := t

     sum := 0

-    share this between maxlock and t

+    share this between waitlevel and t

   }

 

   method Insert(x: int)

-    requires rd(mu) && maxlock << this

+    requires rd(mu) && waitlevel << this

     requires acc(sum,80) && 0 <= x

     ensures rd(mu)

     ensures acc(sum,80) && sum == old(sum) + x

   {

     acquire this

-    assert maxlock == this.mu;

+    assert waitlevel == this.mu;

     sum := sum + x

     var p: Node := head

     acquire p

@@ -47,7 +47,7 @@ class List {
 

     while (p.next != null && p.next.val < x)

       invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)

-      invariant holds(p) && maxlock == p.mu

+      invariant holds(p) && waitlevel == p.mu

       invariant p.next != null ==> acc(p.next.mu,50) && p << p.next

       invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val

       invariant acc(p.sum, 50)

@@ -72,7 +72,7 @@ class List {
   }

 

   method Delete(x: int) returns (wasPresent: bool)

-    requires rd(mu) && maxlock << this

+    requires rd(mu) && waitlevel << this

     requires acc(sum,80) && 0 <= x

     ensures acc(sum,80) && (wasPresent ==> sum == old(sum) - x) && (!wasPresent ==> sum == old(sum))

   {

@@ -87,7 +87,7 @@ class List {
 

     while (p.next != null && p.next.val < x)

       invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)

-      invariant holds(p) && maxlock == p.mu && !assigned(c)

+      invariant holds(p) && waitlevel == p.mu && !assigned(c)

       invariant p.next != null ==> acc(p.next.mu,50) && p << p.next

       invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val

       invariant acc(p.sum, 50)

diff --git a/Chalice/examples/OwickiGries.chalice b/Chalice/examples/OwickiGries.chalice
index 63f029e8..f466b58a 100644
--- a/Chalice/examples/OwickiGries.chalice
+++ b/Chalice/examples/OwickiGries.chalice
@@ -17,7 +17,7 @@ class OwickiGries {
   }

 

   method Worker(b: bool)

-    requires rd(mu) && maxlock << mu

+    requires rd(mu) && waitlevel << mu

     requires (!b ==> acc(c0,50)) && (b ==> acc(c1,50))

     ensures rd(mu)

     ensures !b ==> acc(c0,50) && c0 == old(c0) + 1

diff --git a/Chalice/examples/ProdConsChannel.chalice b/Chalice/examples/ProdConsChannel.chalice
index e8ab1a60..563d72b6 100644
--- a/Chalice/examples/ProdConsChannel.chalice
+++ b/Chalice/examples/ProdConsChannel.chalice
@@ -28,14 +28,14 @@ class Program {
     send ch(null)

   }

   method Consumer(ch: Ch)

-    requires rd(ch.mu) && maxlock << ch.mu

+    requires rd(ch.mu) && waitlevel << ch.mu

     requires credit(ch)

     ensures rd(ch.mu)

   {

     var c: Cell

     receive c := ch

     while (c != null)

-      invariant rd(ch.mu) && maxlock << ch.mu

+      invariant rd(ch.mu) && waitlevel << ch.mu

       invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)

     {

       var i := c.val

@@ -87,14 +87,14 @@ class Program {
     send ch(null)

   }

   method Consumer0(ch: Ch)

-    requires rd(ch.mu) && maxlock << ch.mu

+    requires rd(ch.mu) && waitlevel << ch.mu

     requires credit(ch)

     ensures rd(ch.mu)

   {

     var c: Cell

     receive c := ch

     while (c != null && c.val == 7)  // this consumer may end early, but that's allowed

-      invariant rd(ch.mu) && maxlock << ch.mu

+      invariant rd(ch.mu) && waitlevel << ch.mu

       invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)

     {

       var i := c.val

@@ -102,7 +102,7 @@ class Program {
     }

   }

   method Consumer1(ch: Ch)

-    requires rd(ch.mu) && maxlock << ch.mu

+    requires rd(ch.mu) && waitlevel << ch.mu

     requires credit(ch)

     ensures rd(ch.mu)

   {

@@ -113,7 +113,7 @@ class Program {
     }

   }

   method Consumer2(ch: Ch)

-    requires rd(ch.mu) && maxlock << ch.mu

+    requires rd(ch.mu) && waitlevel << ch.mu

     requires credit(ch)

     ensures rd(ch.mu)

   {

diff --git a/Chalice/examples/Sieve.chalice b/Chalice/examples/Sieve.chalice
index be282402..a7ec9d10 100644
--- a/Chalice/examples/Sieve.chalice
+++ b/Chalice/examples/Sieve.chalice
@@ -18,12 +18,12 @@ class Sieve {
 

   method Filter(prime: int, r: NumberStream, s: NumberStream)

     requires 2 <= prime;

-    requires rd(r.mu) && maxlock << r.mu;

+    requires rd(r.mu) && waitlevel << r.mu;

     requires rd(s.mu) && s.mu << r.mu && credit(r) && credit(s, -1);

   {

     receive x := r;

     while (2 <= x)

-      invariant rd(r.mu) && rd(s.mu) && s << r && maxlock << r.mu;

+      invariant rd(r.mu) && rd(s.mu) && s << r && waitlevel << r.mu;

       invariant 2<= x ==> credit(r);

       invariant credit(s, -1);

     {

@@ -45,12 +45,12 @@ class Sieve {
     while (2 <= p)

       invariant ch != null;

       invariant 2 <= p ==> credit(ch, 1);

-      invariant rd(ch.mu) && maxlock << ch.mu;

+      invariant rd(ch.mu) && waitlevel << ch.mu;

     {

       // print p--it's a prime!

       var cp := new ChalicePrint;  call cp.Int(p);

 

-      var n := new NumberStream between maxlock and ch;

+      var n := new NumberStream between waitlevel and ch;

       fork Filter(p, ch, n);

       ch := n;

       receive p := ch;

diff --git a/Chalice/examples/cell.chalice b/Chalice/examples/cell.chalice
index d4003a3c..1cf82950 100644
--- a/Chalice/examples/cell.chalice
+++ b/Chalice/examples/cell.chalice
@@ -57,7 +57,7 @@ class Interval module Library2 {
     requires 0<=l && l <= r;

     requires acc(left) && acc(right);

     ensures valid;

-    ensures getLeft()==l

+    ensures getLeft()==l;

     ensures getRight()==r;

   {

     left := new Cell;

@@ -143,10 +143,10 @@ class Program module Main {
   }

 

   method main3() returns (rt: Cell)

-    ensures rt!=null && rt.valid && rt.get() == 0

+    ensures rt!=null && rt.valid && rt.get() == 0;

   {

     rt := new Cell;

-    call rt.init(0)

+    call rt.init(0);

   }

 

   method main4() {

diff --git a/Chalice/examples/counter.chalice b/Chalice/examples/counter.chalice
index 0cab7736..828cf005 100644
--- a/Chalice/examples/counter.chalice
+++ b/Chalice/examples/counter.chalice
@@ -34,7 +34,7 @@ class Program {
   }

 

   method bar(c: Counter)

-    requires c!=null && acc(c.mu) && maxlock << c.mu;

+    requires c!=null && acc(c.mu) && waitlevel << c.mu;

     requires eval(c.release, acc(c.value) && 0<=c.value);

   {

     lock (c) {

@@ -81,7 +81,7 @@ class Program {
   }

 

   method foo(c: Counter)

-    requires c!=null && acc(c.mu) && maxlock << c.mu && eval(c.release, acc(c.value) && 10<=c.value);

+    requires c!=null && acc(c.mu) && waitlevel << c.mu && eval(c.release, acc(c.value) && 10<=c.value);

     ensures c!=null && holds(c) && acc(c.mu) && acc(c.value);

     lockchange c;

   {

@@ -93,7 +93,7 @@ class Program {
   }

 

   method nestedGood0(c: Counter)

-    requires c != null && acc(c.mu) && maxlock << c.mu;

+    requires c != null && acc(c.mu) && waitlevel << c.mu;

   {

     lock (c) {

       release c

@@ -102,7 +102,7 @@ class Program {
   }

 

   method nestedGood1(c: Counter)

-    requires c != null && acc(c.mu) && maxlock << c.mu;

+    requires c != null && acc(c.mu) && waitlevel << c.mu;

   {

     var t: Counter := c

     lock (t) {

@@ -114,7 +114,7 @@ class Program {
   }

 

   method nestedBad0(c: Counter)

-    requires c != null && acc(c.mu) && maxlock << c.mu;

+    requires c != null && acc(c.mu) && waitlevel << c.mu;

   {

     lock (c) {

       release c

@@ -122,7 +122,7 @@ class Program {
   }

 

   method nestedBad1(c: Counter)

-    requires c != null && acc(c.mu) && maxlock << c.mu;

+    requires c != null && acc(c.mu) && waitlevel << c.mu;

   {

     lock (c) {

       acquire c  // error: already holds c

@@ -130,7 +130,7 @@ class Program {
   }

 

   method nestedBad2(c: Counter)

-    requires c != null && acc(c.mu) && maxlock << c.mu;

+    requires c != null && acc(c.mu) && waitlevel << c.mu;

   {

     lock (c) {

       lock (c) {  // error: already holds c

@@ -139,7 +139,7 @@ class Program {
   }

 

   method nestedBad3(c: Counter)

-    requires c != null && acc(c.mu) && maxlock << c.mu;

+    requires c != null && acc(c.mu) && waitlevel << c.mu;

   {

     var t: Counter := c

     lock (t) {

diff --git a/Chalice/examples/dining-philosophers.chalice b/Chalice/examples/dining-philosophers.chalice
index 6a67174c..f4a7d1a6 100644
--- a/Chalice/examples/dining-philosophers.chalice
+++ b/Chalice/examples/dining-philosophers.chalice
@@ -17,12 +17,12 @@ class Philosopher module Philosophers {
     requires valid;

     requires acc(getLeft().mu, 10);

     requires acc(getRight().mu, 10);

-    requires maxlock << getLeft().mu;

-    requires maxlock << getRight().mu;

+    requires waitlevel << getLeft().mu;

+    requires waitlevel << getRight().mu;

     requires getLeft().mu << getRight().mu;

   {

     while(true)

-      invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && maxlock << getLeft().mu && maxlock << getRight().mu && getLeft().mu << getRight().mu;

+      invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && waitlevel << getLeft().mu && waitlevel << getRight().mu && getLeft().mu << getRight().mu;

     {

       unfold valid;

       acquire left;

diff --git a/Chalice/examples/producer-consumer.chalice b/Chalice/examples/producer-consumer.chalice
index f2c751d9..99756d65 100644
--- a/Chalice/examples/producer-consumer.chalice
+++ b/Chalice/examples/producer-consumer.chalice
@@ -34,13 +34,13 @@ class Producer module Producer {
   }

 

   method run()

-    requires valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+    requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;

     ensures rd(old(getBuffer()).mu);

   {

     var tmp: int;

 

     while(true)

-      invariant valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+      invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;

     {

       unfold valid;

       acquire buffer;

@@ -75,11 +75,11 @@ class Consumer module Consumer {
   }

 

   method run()

-    requires valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+    requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;

     ensures rd(old(getBuffer()).mu);

   {

     while(true)

-      invariant valid && rd(getBuffer().mu) && maxlock << getBuffer().mu;

+      invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;

     {

       unfold valid;

       acquire buffer;

diff --git a/Chalice/examples/prog0.chalice b/Chalice/examples/prog0.chalice
index 7bcb1505..fb835a24 100644
--- a/Chalice/examples/prog0.chalice
+++ b/Chalice/examples/prog0.chalice
@@ -32,7 +32,7 @@ class C {
     call this.m(2,3,4);

     call a,b,c := o.m();

     call x := m(200);

-    reorder o above maxlock;

+    reorder o above waitlevel;

   }

   method p(a,b,c) returns (x,y,z)

     requires 8 + 2 == 10;

diff --git a/Chalice/examples/prog3.chalice b/Chalice/examples/prog3.chalice
index 6c323d0e..f3b8210b 100644
--- a/Chalice/examples/prog3.chalice
+++ b/Chalice/examples/prog3.chalice
@@ -7,9 +7,9 @@ class Main {
     share d;

 

     var t0: T := new T;  t0.d := d;

-    share t0 between maxlock and d

+    share t0 between waitlevel and d

     var t1: T := new T;  t1.d := d;

-    share t1 between maxlock and d

+    share t1 between waitlevel and d

     

     var t0Token: token<T.run>;

     fork t0Token := t0.run();

@@ -33,15 +33,15 @@ class Main {
     fork uToken := u.run();

 

     acquire u;  // a little unusual to acquire after a fork, but allowed

-    assert maxlock == u.mu;

+    assert waitlevel == u.mu;

 

     var v := new U;

-    share v;  acquire v;  // this line has the effect of increasing maxlock

+    share v;  acquire v;  // this line has the effect of increasing waitlevel

 

-    assert maxlock == v.mu;

-    assert maxlock != u.mu;

+    assert waitlevel == v.mu;

+    assert waitlevel != u.mu;

     assert u << v;

-    assert u << maxlock;

+    assert u << waitlevel;

 

     join uToken;  // material for the smoke check

     release u;

@@ -49,7 +49,7 @@ class Main {
   }

   

   method C()

-    ensures maxlock == old(maxlock);

+    ensures waitlevel == old(waitlevel);

   {

     var u := new U;

     share u;

@@ -65,23 +65,23 @@ class Main {
   {

   }

   method MxCaller0()

-    ensures maxlock == old(maxlock);

+    ensures waitlevel == old(waitlevel);

   {

   }

   method MxCaller1()

-    ensures maxlock == old(maxlock);

+    ensures waitlevel == old(waitlevel);

   {

     call Mx0();

   }

   method MxCaller2()

-    ensures maxlock == old(maxlock); // error

+    ensures waitlevel == old(waitlevel); // error

   {

     call Mx1();

   }  // error: missing lockchange

 

   method D(u: U)

-    requires u != null && rd(u.mu) && maxlock << u;

-    ensures maxlock == old(maxlock);

+    requires u != null && rd(u.mu) && waitlevel << u;

+    ensures waitlevel == old(waitlevel);

   {

     acquire u;

     release u;

@@ -103,7 +103,7 @@ class T {
   var d: Data;

   invariant rd(d) && d != null && rd(d.mu) && rd(this.mu) && this << d;

   method run()

-    requires rd(mu) && maxlock << this;

+    requires rd(mu) && waitlevel << this;

     ensures rd(mu);

   {

     acquire this;

@@ -117,7 +117,7 @@ class T {
 

 class U {

   method run()

-    requires rd(mu) && maxlock << this;

+    requires rd(mu) && waitlevel << this;

     ensures rd(mu);

   {

   }

diff --git a/Chalice/examples/prog4.chalice b/Chalice/examples/prog4.chalice
index 655c5815..bc6aef99 100644
--- a/Chalice/examples/prog4.chalice
+++ b/Chalice/examples/prog4.chalice
@@ -22,7 +22,7 @@ class LoopTargets {
     acquire t

     var s := true

     while (s)

-      invariant acc(t.mu) && maxlock == t.mu

+      invariant acc(t.mu) && waitlevel == t.mu

     {

       release t  // error: loop invariant does not say holds(t) (414)

       acquire t

@@ -37,7 +37,7 @@ class LoopTargets {
     var s := true

     while (s)

       invariant rd(t.mu)

-      invariant holds(t) && maxlock == t.mu

+      invariant holds(t) && waitlevel == t.mu

     {

       release t

       acquire t

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index b60ce521..c353a5ba 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -7,274 +7,274 @@ import scala.util.parsing.input.Position
 import scala.util.parsing.input.NoPosition

 

 object Boogie {

-  

-  sealed abstract class Decl

-  case class Const(id: String, unique: boolean, t: BType) extends Decl

-  case class Proc(id: String, ins: List[BVar], outs: List[BVar],

-                  mod: List[String], PrePost: List[String],

-                  body: List[Stmt]) extends Decl

-  case class Function(id: String, ins: List[BVar], out: BVar) extends Decl

-  case class Axiom(expr: Expr) extends Decl

+ 

+ sealed abstract class Decl

+ case class Const(id: String, unique: boolean, t: BType) extends Decl

+ case class Proc(id: String, ins: List[BVar], outs: List[BVar],

+                 mod: List[String], PrePost: List[String],

+                 body: List[Stmt]) extends Decl

+ case class Function(id: String, ins: List[BVar], out: BVar) extends Decl

+ case class Axiom(expr: Expr) extends Decl

 

-  sealed abstract class BType

-  case class NamedType(s: String) extends BType

-  case class ClassType(cl: Class) extends BType

-  case class IndexedType(id: String, t: BType) extends BType

+ sealed abstract class BType

+ case class NamedType(s: String) extends BType

+ case class ClassType(cl: Class) extends BType

+ case class IndexedType(id: String, t: BType) extends BType

 

-  sealed abstract class Stmt {

-    def Locals = List[BVar]()

-  }

-  case class Comment(comment: String) extends Stmt

-  case class Assert(e: Expr) extends Stmt {

-    def this(e: Expr, p: Position, txt: String) = { this(e); this.pos = p; this.message = txt; this } 

-    var pos = NoPosition : Position

-    var message = "" : String

-  }

-  case class Assume(e: Expr) extends Stmt

-  case class Assign(lhs: Expr, rhs: Expr) extends Stmt

-  case class AssignMap(lhs: Expr, index: Expr, rhs: Expr) extends Stmt

-  case class Havoc(x: Expr) extends Stmt

-  case class MapUpdate(map: Expr, arg0: Expr, arg1: String, rhs: Expr) extends Stmt {

-    def this(map: Expr, arg0: Expr, rhs: Expr) = this(map, arg0, null, rhs)

-  }

-  case class If(guard: Expr, thn: List[Stmt], els: List[Stmt]) extends Stmt {

-    override def Locals = (thn flatMap (_.Locals)) ::: (els flatMap (_.Locals))

-  }

-  case class LocalVar(x: BVar) extends Stmt {

-    def this(id: String, tp: BType) = this(BVar(id, tp))

+ sealed abstract class Stmt {

+   def Locals = List[BVar]()

+ }

+ case class Comment(comment: String) extends Stmt

+ case class Assert(e: Expr) extends Stmt {

+   def this(e: Expr, p: Position, txt: String) = { this(e); this.pos = p; this.message = txt; this } 

+   var pos = NoPosition : Position

+   var message = "" : String

+ }

+ case class Assume(e: Expr) extends Stmt

+ case class Assign(lhs: Expr, rhs: Expr) extends Stmt

+ case class AssignMap(lhs: Expr, index: Expr, rhs: Expr) extends Stmt

+ case class Havoc(x: Expr) extends Stmt

+ case class MapUpdate(map: Expr, arg0: Expr, arg1: String, rhs: Expr) extends Stmt {

+   def this(map: Expr, arg0: Expr, rhs: Expr) = this(map, arg0, null, rhs)

+ }

+ case class If(guard: Expr, thn: List[Stmt], els: List[Stmt]) extends Stmt {

+   override def Locals = (thn flatMap (_.Locals)) ::: (els flatMap (_.Locals))

+ }

+ case class LocalVar(x: BVar) extends Stmt {

+   def this(id: String, tp: BType) = this(BVar(id, tp))

 

-    override def Locals = List(x)

-  }

+   override def Locals = List(x)

+ }

 

-  sealed abstract class Expr {

-    def &&(that: Expr) = BinaryExpr("&&", this, that)

-    def ||(that: Expr) = BinaryExpr("||", this, that)

-    def ==@(that: Expr) = BinaryExpr("==", this, that)

-    def !=@(that: Expr) = BinaryExpr("!=", this, that)

-    def Equals(that: Expr) = BinaryExpr("==", this, that)

-    def ==>(that: Expr) = BinaryExpr("==>", this, that)

-    def <==>(that: Expr) = BinaryExpr("<==>", this, that)

-    def unary_! = UnaryExpr("!", this)

-    def <=(that: Expr) = BinaryExpr("<=", this, that)

-    def <(that: Expr) = BinaryExpr("<", this, that)

-    def >=(that: Expr) = BinaryExpr(">=", this, that)

-    def >(that: Expr) = BinaryExpr(">", this, that)

-    def +(that: Expr) = BinaryExpr("+", this, that)

-    def -(that: Expr) = BinaryExpr("-", this, that)

-    def *(that: Expr) = BinaryExpr("*", this, that)

-    def /(that: Expr) = BinaryExpr("/", this, that)

-    def %(that: Expr) = BinaryExpr("%", this, that)

-    def := (that: Expr) = Assign(this, that)

-    def select(e: Expr, f: Expr) = new MapSelect(this, e, PrintExpr(f))

-    def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, PrintExpr(f), rhs)

-  }

-  case class IntLiteral(n: int) extends Expr

-  case class BoolLiteral(b: boolean) extends Expr

-  case class Null extends Expr

-  case class VarExpr(id: String) extends Expr {

-    def this(v: BVar) = this(v.id)

-  }

-  case class MapSelect(map: Expr, arg0: Expr, arg1: String) extends Expr {

-    def this(map: Expr, arg0: Expr) = this(map, arg0, null) // for one-dimensional maps

-    def this(map: Expr, arg0: Expr, arg1: String, arg2: String) = // for 3-dimensional maps

-      this(MapSelect(map, arg0, arg1), VarExpr(arg2), null)

-  }

-  case class MapStore(map: Expr, arg0: String, rhs: Expr) extends Expr

-  case class Old(e: Expr) extends Expr

-  case class UnaryExpr(op: String, e: Expr) extends Expr

-  case class BinaryExpr(op: String, e0: Expr, e1: Expr) extends Expr

-  case class FunctionApp(f: String, args: List[Expr]) extends Expr {

-    def this(f: String, a0: Expr) = this(f, List(a0))

-    def this(f: String, a0: Expr, a1: Expr) = this(f, List(a0, a1))

-    def this(f: String, a0: Expr, a1: Expr, a2: Expr) = this(f, List(a0, a1, a2))

-  }

-  case class Forall(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {

-    def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(List(), xs, triggers, body)

-    def this(x: BVar, body: Expr) = this(List(), List(x), List(), body)

-    def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), List(), body)

-  }

-  case class Exists(xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {

-    def this(x: BVar, body: Expr) = this(List(x), List(), body)

-  }

-  case class Ite(con: Expr, then: Expr, els: Expr) extends Expr

+ sealed abstract class Expr {

+   def &&(that: Expr) = BinaryExpr("&&", this, that)

+   def ||(that: Expr) = BinaryExpr("||", this, that)

+   def ==@(that: Expr) = BinaryExpr("==", this, that)

+   def !=@(that: Expr) = BinaryExpr("!=", this, that)

+   def Equals(that: Expr) = BinaryExpr("==", this, that)

+   def ==>(that: Expr) = BinaryExpr("==>", this, that)

+   def <==>(that: Expr) = BinaryExpr("<==>", this, that)

+   def unary_! = UnaryExpr("!", this)

+   def <=(that: Expr) = BinaryExpr("<=", this, that)

+   def <(that: Expr) = BinaryExpr("<", this, that)

+   def >=(that: Expr) = BinaryExpr(">=", this, that)

+   def >(that: Expr) = BinaryExpr(">", this, that)

+   def +(that: Expr) = BinaryExpr("+", this, that)

+   def -(that: Expr) = BinaryExpr("-", this, that)

+   def *(that: Expr) = BinaryExpr("*", this, that)

+   def /(that: Expr) = BinaryExpr("/", this, that)

+   def %(that: Expr) = BinaryExpr("%", this, that)

+   def := (that: Expr) = Assign(this, that)

+   def select(e: Expr, f: Expr) = new MapSelect(this, e, PrintExpr(f))

+   def store(e: Expr, f: Expr, rhs: Expr) = MapUpdate(this, e, PrintExpr(f), rhs)

+ }

+ case class IntLiteral(n: int) extends Expr

+ case class BoolLiteral(b: boolean) extends Expr

+ case class Null extends Expr

+ case class VarExpr(id: String) extends Expr {

+   def this(v: BVar) = this(v.id)

+ }

+ case class MapSelect(map: Expr, arg0: Expr, arg1: String) extends Expr {

+   def this(map: Expr, arg0: Expr) = this(map, arg0, null) // for one-dimensional maps

+   def this(map: Expr, arg0: Expr, arg1: String, arg2: String) = // for 3-dimensional maps

+     this(MapSelect(map, arg0, arg1), VarExpr(arg2), null)

+ }

+ case class MapStore(map: Expr, arg0: String, rhs: Expr) extends Expr

+ case class Old(e: Expr) extends Expr

+ case class UnaryExpr(op: String, e: Expr) extends Expr

+ case class BinaryExpr(op: String, e0: Expr, e1: Expr) extends Expr

+ case class FunctionApp(f: String, args: List[Expr]) extends Expr {

+   def this(f: String, a0: Expr) = this(f, List(a0))

+   def this(f: String, a0: Expr, a1: Expr) = this(f, List(a0, a1))

+   def this(f: String, a0: Expr, a1: Expr, a2: Expr) = this(f, List(a0, a1, a2))

+ }

+ case class Forall(ta: List[TVar], xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {

+   def this(xs: List[BVar], triggers: List[Expr], body: Expr) = this(List(), xs, triggers, body)

+   def this(x: BVar, body: Expr) = this(List(), List(x), List(), body)

+   def this(t: TVar, x: BVar, body: Expr) = this(List(t), List(x), List(), body)

+ }

+ case class Exists(xs: List[BVar], triggers: List[Expr], body: Expr) extends Expr {

+   def this(x: BVar, body: Expr) = this(List(x), List(), body)

+ }

+ case class Ite(con: Expr, then: Expr, els: Expr) extends Expr

 

-  case class BVar(id: String, t: BType) {

-    def this(id: String, t: BType, uniquifyName: boolean) =

-      this(if (uniquifyName) {

-             val n = S_BVar.VariableCount

-             S_BVar.VariableCount = S_BVar.VariableCount + 1

-             id + "#_" + n

-           } else {

-             id

-           }, t)

-    val where: Expr = null

-  }

-  object S_BVar { var VariableCount = 0 }

-  def NewBVar(id: String, t: BType, uniquifyName: boolean) = {

-    val v = new Boogie.BVar(id, t, uniquifyName)

-    val e = new Boogie.VarExpr(v)

-    (v,e)

-  }

-  case class TVar(id: String) {

-    def this(id: String, uniquifyName: boolean) =

-      this(if (uniquifyName) {

-             val n = S_TVar.VariableCount

-             S_TVar.VariableCount = S_TVar.VariableCount + 1

-             id + "#_" + n

-           } else {

-             id

-           })

-    val where: Expr = null

-  }

-  object S_TVar { var VariableCount = 0 }

-  def NewTVar(id: String) = {

-    val v = new Boogie.TVar(id, true)

-    val e = new Boogie.NamedType(v.id)

-    (v,e)

-  }

+ case class BVar(id: String, t: BType) {

+   def this(id: String, t: BType, uniquifyName: boolean) =

+     this(if (uniquifyName) {

+            val n = S_BVar.VariableCount

+            S_BVar.VariableCount = S_BVar.VariableCount + 1

+            id + "#_" + n

+          } else {

+            id

+          }, t)

+   val where: Expr = null

+ }

+ object S_BVar { var VariableCount = 0 }

+ def NewBVar(id: String, t: BType, uniquifyName: boolean) = {

+   val v = new Boogie.BVar(id, t, uniquifyName)

+   val e = new Boogie.VarExpr(v)

+   (v,e)

+ }

+ case class TVar(id: String) {

+   def this(id: String, uniquifyName: boolean) =

+     this(if (uniquifyName) {

+            val n = S_TVar.VariableCount

+            S_TVar.VariableCount = S_TVar.VariableCount + 1

+            id + "#_" + n

+          } else {

+            id

+          })

+   val where: Expr = null

+ }

+ object S_TVar { var VariableCount = 0 }

+ def NewTVar(id: String) = {

+   val v = new Boogie.TVar(id, true)

+   val e = new Boogie.NamedType(v.id)

+   (v,e)

+ }

 

-  var vsMode = false;  // global variable settable from outside the class (non-ideal design)

+ var vsMode = false;  // global variable settable from outside the class (non-ideal design)

 

-  // def out(s: String) = Console.out.print(s)

-  var indentLevel = 1

-  def indent: String = {

-    def doIndent(i: int): String = {

-      if(i==0) { "" } else { "  " + doIndent(i-1) }

-    }

-    doIndent(indentLevel);

-  }

+ // def out(s: String) = Console.out.print(s)

+ var indentLevel = 1

+ def indent: String = {

+   def doIndent(i: int): String = {

+     if(i==0) { "" } else { "  " + doIndent(i-1) }

+   }

+   doIndent(indentLevel);

+ }

 

-  def IndentMore(what: => String) = {

-    val prev = indentLevel

-    indentLevel = indentLevel + 1

-    val result = what

-    indentLevel = prev

-    result

-  }

-  def nl = System.getProperty("line.separator");

-  

-  def Print[T](list: List[T], sep: String, p: T => String): String = list match {

-    case Nil => ""

-    case x :: Nil => p(x)

-    case x :: xs => p(x) + sep + Print(xs, sep, p)

-  }

-  def PrintType(t: BType): String = t match {

-    case nt@ NamedType(s) =>

-      s

-    case ClassType(cl) =>

-      if (cl.IsRef) "ref" else cl.id

-    case IndexedType(id,t) =>

-      id + " (" + PrintType(t) + ")"

-  }

-  def Print(d: Decl): String = d match {

-    case Const(id, u, t) =>

-      "const " + (if (u) "unique " else "" ) + id + ": " + PrintType(t) + ";" + nl

-    case p: Proc =>

-      "procedure " + p.id +

-      "(" + Print(p.ins, ", ", PrintVar) + ")" +

-      " returns (" + Print(p.outs, ", ", PrintVar) + ")" + nl + 

-      (p.mod match {

-        case Nil => ""

-        case x :: xs =>

-          indent +  "modifies " +

-          Print(p.mod, ", ", { s: String => s }) +

-          ";" + nl

-      }) + 

-      Print(p.PrePost, nl, { spec: String => indent + spec }) + nl +

-      "{" + nl + 

-      Print(p.body flatMap (_.Locals), "", { v:BVar => indent + "var " + PrintVar(v) + ";" + nl}) + 

-      Print(p.body, "", PrintStmt) + 

-      "}" + nl

-    case Function(id, ins, out) =>

-      "function " + id + "(" + Print(ins, ", ", PrintVar) + ") returns (" + PrintVar(out) + ");" + nl

-    case Axiom(e) =>

-      "axiom " + PrintExpr(e) + ";" + nl

-  }

-  def PrintVar(v: BVar): String = {

-    v.id + ": " + PrintType(v.t) +

-    (if (v.where != null) {" where " + PrintExpr(v.where) } else { "" })

-  }

-  def PrintStmt(s: Stmt): String = s match {

-    case Comment(msg) => indent +  "// " +  msg + nl

-    case assert@Assert(e) =>

-      val pos = if (vsMode) {

-        val r = assert.pos.line - 1;

-        val c = assert.pos.column - 1;

-        r + "," + c + "," + r + "," + (c+5) + ":"

-      } else {

-        "  " + assert.pos + ": "

-      }

-      indent +  "assert " + "{:msg \"" + pos + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl

-    case Assume(e) => indent + "assume " + PrintExpr(e) +  ";" + nl

-    case If(guard, thn, els) =>

-      indent + "if (" +

-      (if (guard == null) "*" else PrintExpr(guard)) +

-      ") {" +  nl + 

-      IndentMore { Print(thn, "", PrintStmt)  } + 

-      indent +  "} else {"  + nl + 

-      IndentMore { Print(els, "", PrintStmt)  } + 

-      indent + "}" + nl

-    case Assign(lhs, rhs) =>

-      indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl

-    case AssignMap(lhs, index, rhs) =>

-      indent + PrintExpr(lhs) + "[" + PrintExpr(index) + "] := " + PrintExpr(rhs) + ";" + nl

-    case Havoc(lhs) =>

-      indent + "havoc " + PrintExpr(lhs) + ";" + nl

-    case MapUpdate(map, a0, a1, rhs) =>

-      indent + PrintExpr(map) + "[" +

-      PrintExpr(a0) +

-      (if (a1 != null) { ", " + a1 } else { "" }) +

-      "] := " + 

-      PrintExpr(rhs) + ";" + nl

-    case _:LocalVar => "" /* print nothing */

-  }

-  def PrintExpr(e: Expr): String = {

-    PrintExpr(e, false)

-  }

-  def PrintExpr(e: Expr, useParens: boolean): String = e match {

-    case IntLiteral(n) => n.toString

-    case BoolLiteral(b) => b.toString

-    case Null() => "null"

-    case VarExpr(id) => id

-    case MapSelect(map, arg0, arg1) =>

-      PrintExpr(map) + "[" + PrintExpr(arg0, false) + 

-      (if (arg1 != null) { ", " + arg1 } else { "" }) +

-      "]"

-    case MapStore(map, arg0, rhs) =>

-      PrintExpr(map) + "[" + arg0 + " := " + PrintExpr(rhs, false) + "]"

-    case Old(e) => "old(" + PrintExpr(e, false) + ")"

-    case UnaryExpr(op, e) =>

-      (if (useParens)  { "(" } else "") +

-      op + PrintExpr(e, true) +

-      (if (useParens) ")" else "" )

-    case BinaryExpr(op, e0, e1) =>

-      // reduce parentheses in a special common case:

-      val binIsAndImpIff = op=="&&" || op=="==>" || op=="<==>";

-      def IsAnd(e: Expr) = e match { case BinaryExpr(op,_,_) if op=="&&" => true case _ => false }

-      (if (useParens) "(" else "") + PrintExpr(e0, !(binIsAndImpIff && IsAnd(e0))) + 

-      " " + op + " " + 

-      PrintExpr(e1, !(binIsAndImpIff && IsAnd(e1))) +

-      (if (useParens) ")" else "")

-    case FunctionApp(f, args) =>

-      f + "(" +

-      Print(args, ", ", { e: Expr => PrintExpr(e, false) }) +

-      ")"

-    case Ite(con, then, els) =>

-      "ite(" + PrintExpr(con) + ", " + PrintExpr(then) + ", " + PrintExpr(els) + ")"

-    case Forall(ts, xs, triggers, body) =>

-      "(forall" +

-      (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") +

-      Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +

-      " :: " +

-      Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +

-      PrintExpr(body) +

-      ")"

-    case Exists(xs, triggers, body) =>

-      "(exists " +

-      Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +

-      " :: " +

-      Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +

-      PrintExpr(body) +

-      ")"

-  }

+ def IndentMore(what: => String) = {

+   val prev = indentLevel

+   indentLevel = indentLevel + 1

+   val result = what

+   indentLevel = prev

+   result

+ }

+ def nl = System.getProperty("line.separator");

+ 

+ def Print[T](list: List[T], sep: String, p: T => String): String = list match {

+   case Nil => ""

+   case x :: Nil => p(x)

+   case x :: xs => p(x) + sep + Print(xs, sep, p)

+ }

+ def PrintType(t: BType): String = t match {

+   case nt@ NamedType(s) =>

+     s

+   case ClassType(cl) =>

+     if (cl.IsRef) "ref" else cl.id

+   case IndexedType(id,t) =>

+     id + " (" + PrintType(t) + ")"

+ }

+ def Print(d: Decl): String = d match {

+   case Const(id, u, t) =>

+     "const " + (if (u) "unique " else "" ) + id + ": " + PrintType(t) + ";" + nl

+   case p: Proc =>

+     "procedure " + p.id +

+     "(" + Print(p.ins, ", ", PrintVar) + ")" +

+     " returns (" + Print(p.outs, ", ", PrintVar) + ")" + nl + 

+     (p.mod match {

+       case Nil => ""

+       case x :: xs =>

+         indent +  "modifies " +

+         Print(p.mod, ", ", { s: String => s }) +

+         ";" + nl

+     }) + 

+     Print(p.PrePost, nl, { spec: String => indent + spec }) + nl +

+     "{" + nl + 

+     Print(p.body flatMap (_.Locals), "", { v:BVar => indent + "var " + PrintVar(v) + ";" + nl}) + 

+     Print(p.body, "", PrintStmt) + 

+     "}" + nl

+   case Function(id, ins, out) =>

+     "function " + id + "(" + Print(ins, ", ", PrintVar) + ") returns (" + PrintVar(out) + ");" + nl

+   case Axiom(e) =>

+     "axiom " + PrintExpr(e) + ";" + nl

+ }

+ def PrintVar(v: BVar): String = {

+   v.id + ": " + PrintType(v.t) +

+   (if (v.where != null) {" where " + PrintExpr(v.where) } else { "" })

+ }

+ def PrintStmt(s: Stmt): String = s match {

+   case Comment(msg) => indent +  "// " +  msg + nl

+   case assert@Assert(e) =>

+     val pos = if (vsMode) {

+       val r = assert.pos.line - 1;

+       val c = assert.pos.column - 1;

+       r + "," + c + "," + r + "," + (c+5) + ":"

+     } else {

+       "  " + assert.pos + ": "

+     }

+     indent +  "assert " + "{:msg \"" + pos + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl

+   case Assume(e) => indent + "assume " + PrintExpr(e) +  ";" + nl

+   case If(guard, thn, els) =>

+     indent + "if (" +

+     (if (guard == null) "*" else PrintExpr(guard)) +

+     ") {" +  nl + 

+     IndentMore { Print(thn, "", PrintStmt)  } + 

+     indent +  "} else {"  + nl + 

+     IndentMore { Print(els, "", PrintStmt)  } + 

+     indent + "}" + nl

+   case Assign(lhs, rhs) =>

+     indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl

+   case AssignMap(lhs, index, rhs) =>

+     indent + PrintExpr(lhs) + "[" + PrintExpr(index) + "] := " + PrintExpr(rhs) + ";" + nl

+   case Havoc(lhs) =>

+     indent + "havoc " + PrintExpr(lhs) + ";" + nl

+   case MapUpdate(map, a0, a1, rhs) =>

+     indent + PrintExpr(map) + "[" +

+     PrintExpr(a0) +

+     (if (a1 != null) { ", " + a1 } else { "" }) +

+     "] := " + 

+     PrintExpr(rhs) + ";" + nl

+   case _:LocalVar => "" /* print nothing */

+ }

+ def PrintExpr(e: Expr): String = {

+   PrintExpr(e, false)

+ }

+ def PrintExpr(e: Expr, useParens: boolean): String = e match {

+   case IntLiteral(n) => n.toString

+   case BoolLiteral(b) => b.toString

+   case Null() => "null"

+   case VarExpr(id) => id

+   case MapSelect(map, arg0, arg1) =>

+     PrintExpr(map) + "[" + PrintExpr(arg0, false) + 

+     (if (arg1 != null) { ", " + arg1 } else { "" }) +

+     "]"

+   case MapStore(map, arg0, rhs) =>

+     PrintExpr(map) + "[" + arg0 + " := " + PrintExpr(rhs, false) + "]"

+   case Old(e) => "old(" + PrintExpr(e, false) + ")"

+   case UnaryExpr(op, e) =>

+     (if (useParens)  { "(" } else "") +

+     op + PrintExpr(e, true) +

+     (if (useParens) ")" else "" )

+   case BinaryExpr(op, e0, e1) =>

+     // reduce parentheses in a special common case:

+     val binIsAndImpIff = op=="&&" || op=="==>" || op=="<==>";

+     def IsAnd(e: Expr) = e match { case BinaryExpr(op,_,_) if op=="&&" => true case _ => false }

+     (if (useParens) "(" else "") + PrintExpr(e0, !(binIsAndImpIff && IsAnd(e0))) + 

+     " " + op + " " + 

+     PrintExpr(e1, !(binIsAndImpIff && IsAnd(e1))) +

+     (if (useParens) ")" else "")

+   case FunctionApp(f, args) =>

+     f + "(" +

+     Print(args, ", ", { e: Expr => PrintExpr(e, false) }) +

+     ")"

+   case Ite(con, then, els) =>

+     "ite(" + PrintExpr(con) + ", " + PrintExpr(then) + ", " + PrintExpr(els) + ")"

+   case Forall(ts, xs, triggers, body) =>

+     "(forall" +

+     (if (ts.length == 0) " " else "<" + Print(ts, ", ", { x: TVar => x.id }) + "> ") +

+     Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +

+     " :: " +

+     Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +

+     PrintExpr(body) +

+     ")"

+   case Exists(xs, triggers, body) =>

+     "(exists " +

+     Print(xs, ", ", { x: BVar => x.id +  ": " + PrintType(x.t) }) +

+     " :: " +

+     Print(triggers , "", { s: Expr => "{" + PrintExpr(s) + "} " }) +

+     PrintExpr(body) +

+     ")"

+ }

 }

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 1a6e3e48..2f54b71f 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -10,125 +10,128 @@ import java.io.FileWriter
 import scala.util.parsing.input.Position

 

 object Chalice {

-  def main(args: Array[String]): unit = {

-    var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

-    // parse command-line arguments

-    var inputName: String = null

-    var printProgram = false

-    var vsMode = false;

-    def ReportError(pos: Position, msg: String) = {

-      if (vsMode) {

-        val r = pos.line - 1;

-        val c = pos.column - 1;

-        Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);

-      } else {

-        Console.err.println(pos + ": " + msg)

-      }

-    }

-    var doTypecheck = true

-    var doTranslate = true

-    var checkLeaks = false

-    // level 0 or below: no defaults

-    // level 1: unfold predicates with receiver this in pre and postconditions

-    // level 2: unfold predicates and functions with receiver this in pre and postconditions

-    // level 3 or above: level 2 + autoMagic

-    var defaults = 0

-    var autoFold = false

-    var autoMagic = false

-    var skipDeadlockChecks = false

-    var boogieArgs = " ";

-    var gen = false;

+ def main(args: Array[String]): unit = {

+   var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

+   // parse command-line arguments

+   var inputName: String = null

+   var printProgram = false

+   var vsMode = false;

+   def ReportError(pos: Position, msg: String) = {

+     if (vsMode) {

+       val r = pos.line - 1;

+       val c = pos.column - 1;

+       Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);

+     } else {

+       Console.err.println(pos + ": " + msg)

+     }

+   }

+   var doTypecheck = true

+   var doTranslate = true

+   var checkLeaks = false

+   // level 0 or below: no defaults

+   // level 1: unfold predicates with receiver this in pre and postconditions

+   // level 2: unfold predicates and functions with receiver this in pre and postconditions

+   // level 3 or above: level 2 + autoMagic

+   var defaults = 0

+   var autoFold = false

+   var autoMagic = false

+   var skipDeadlockChecks = false

+   var boogieArgs = " ";

+   var gen = false;

 

-    for (a <- args) {

-      if (a == "-print") printProgram = true

-      else if (a == "-noTranslate") doTranslate = false

-      else if (a == "-noTypecheck") doTypecheck = false

-      else if (a == "-vs") vsMode = true

-      else if (a == "-checkLeaks") checkLeaks = true

-      else if (a == "-noDeadlockChecks") skipDeadlockChecks = true

-      else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)

-      else if (a == "-defaults") defaults = 3

-      else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } }

-      else if (a == "-gen") { gen = true; }

-      else if (a == "-autoFold") autoFold = true

-      else if (a == "-autoMagic") autoMagic = true

-      else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe

-      else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a); return }

-      else { inputName = a }

-    }

-    // check the command-line arguments

-    if (inputName == null) { CommandLineError("missing input filename"); return } else {

-      val file = new File(inputName);

-      if(! file.exists()){

-        CommandLineError("input file " + file.getName() + " could not be found"); return

-      }

-    }

-    // parse program

-    val parser = new Parser();

-    parser.parseFile(inputName) match {

-      case e: parser.NoSuccess =>

-        if (vsMode)

-          ReportError(e.next.pos, e.msg);

-        else

-          Console.err.println("Error: " + e)

-      case parser.Success(prog, _) =>

-        if (printProgram) PrintProgram.P(prog)

-        if (doTypecheck) {

-          // typecheck program

-          Resolver.Resolve(prog) match {

-            case Resolver.Errors(msgs) => 

-              if (!vsMode) Console.err.println("The program did not typecheck.");

-              msgs foreach { msg => ReportError(msg._1, msg._2) }

-            case Resolver.Success() =>

-              if (doTranslate) {

-                // checking if Boogie.exe exists

-                val boogieFile = new File(boogiePath);

-                if(! boogieFile.exists() || ! boogieFile.isFile()) {

-                  CommandLineError("Boogie.exe not found at " + boogiePath); return

-                }

-                // translate program to Boogie

-                val translator = new Translator();

-                // set the translation options

-                TranslationOptions.checkLeaks = checkLeaks;

-                TranslationOptions.defaults = defaults;

-                TranslationOptions.autoFold = autoFold;

-                TranslationOptions.autoMagic = autoMagic;

-                TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;

-                val bplProg = translator.translateProgram(prog);

-                // write to out.bpl

-                Boogie.vsMode = vsMode;

-                val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

-                writeFile("out.bpl", bplText);

-                // run Boogie.exe on out.bpl

-                val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + "out.bpl"); 

-                val input = new BufferedReader(new InputStreamReader(boogie.getInputStream()));

-                var line = input.readLine();

-                var previous_line = null: String;

-                while(line!=null){

-                  println(line);

-                  previous_line = line;

-                  line = input.readLine();

-                }

-                if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

-                  val converter = new ChaliceToCSharp(); 

-                  println("Code generated in out.cs.");

-                  writeFile("out.cs", converter.convertProgram(prog));

-                }

-              }

-            }

-        }

-    }

-  }

+   for (a <- args) {

+     if (a == "-print") printProgram = true

+     else if (a == "-noTranslate") doTranslate = false

+     else if (a == "-noTypecheck") doTypecheck = false

+     else if (a == "-vs") vsMode = true

+     else if (a == "-checkLeaks") checkLeaks = true

+     else if (a == "-noDeadlockChecks") skipDeadlockChecks = true

+     else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)

+     else if (a == "-defaults") defaults = 3

+     else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } }

+     else if (a == "-gen") { gen = true; }

+     else if (a == "-autoFold") autoFold = true

+     else if (a == "-autoMagic") autoMagic = true

+     else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // arguments starting with "-" or "/" are sent to Boogie.exe

+     else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a); return }

+     else { inputName = a }

+   }

+   // check the command-line arguments

+   if (inputName == null && vsMode) {

+     inputName = "<stdin>"

+   } else if (inputName == null) { CommandLineError("missing input filename"); return } else {

+     val file = new File(inputName);

+     if(! file.exists()){

+       CommandLineError("input file " + file.getName() + " could not be found"); return

+     }

+   }

+   // parse program

+   val parser = new Parser();

+   parser.parseFile(inputName) match {

+     case e: parser.NoSuccess =>

+       if (vsMode)

+         ReportError(e.next.pos, e.msg);

+       else

+         Console.err.println("Error: " + e)

+     case parser.Success(prog, _) =>

+       if (printProgram) PrintProgram.P(prog)

+       if (doTypecheck) {

+         // typecheck program

+         Resolver.Resolve(prog) match {

+           case Resolver.Errors(msgs) => 

+             if (!vsMode) Console.err.println("The program did not typecheck.");

+             msgs foreach { msg => ReportError(msg._1, msg._2) }

+           case Resolver.Success() =>

+             if (doTranslate) {

+               // checking if Boogie.exe exists

+               val boogieFile = new File(boogiePath);

+               if(! boogieFile.exists() || ! boogieFile.isFile()) {

+                 CommandLineError("Boogie.exe not found at " + boogiePath); return

+               }

+               // translate program to Boogie

+               val translator = new Translator();

+               // set the translation options

+               TranslationOptions.checkLeaks = checkLeaks;

+               TranslationOptions.defaults = defaults;

+               TranslationOptions.autoFold = autoFold;

+               TranslationOptions.autoMagic = autoMagic;

+               TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;

+               val bplProg = translator.translateProgram(prog);

+               // write to out.bpl

+               Boogie.vsMode = vsMode;

+               val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

+               val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl"

+               writeFile(bplFilename, bplText);

+               // run Boogie.exe on out.bpl

+               val boogie = Runtime.getRuntime().exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename);

+               val input = new BufferedReader(new InputStreamReader(boogie.getInputStream()));

+               var line = input.readLine();

+               var previous_line = null: String;

+               while(line!=null){

+                 println(line);

+                 previous_line = line;

+                 line = input.readLine();

+               }

+               if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

+                 val converter = new ChaliceToCSharp(); 

+                 println("Code generated in out.cs.");

+                 writeFile("out.cs", converter.convertProgram(prog));

+               }

+             }

+           }

+       }

+   }

+ }

 

-  def writeFile(filename: String, text: String) {

-    val writer = new FileWriter(new File(filename));

-    writer.write(text);

-    writer.flush();

-    writer.close();

-  }

+ def writeFile(filename: String, text: String) {

+   val writer = new FileWriter(new File(filename));

+   writer.write(text);

+   writer.flush();

+   writer.close();

+ }

 

-  def CommandLineError(msg: String) = {

-    Console.err.println("Error: " + msg)

-    Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-vs] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")

-  }

+ def CommandLineError(msg: String) = {

+   Console.err.println("Error: " + msg)

+   Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-vs] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")

+ }

 }

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 4442526f..98ba0416 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -13,7 +13,11 @@ import scala.util.parsing.input.NoPosition
 class Parser extends StandardTokenParsers {

 

   def parseFile(path: String): this.ParseResult[List[TopLevelDecl]] = {

-    val tokens = new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path));

+    val tokens = if (path == "<stdin>") {

+        new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in))

+      } else {

+        new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path));

+      }

     phrase(programUnit)(tokens)

   }

  

@@ -25,7 +29,7 @@ class Parser extends StandardTokenParsers {
                        "lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned",

                        "call", "if", "else", "while", "invariant", "lockchange",

                        "returns", "requires", "ensures", "where",

-                       "int", "bool", "false", "true", "null", "maxlock", "lockbottom",

+                       "int", "bool", "false", "true", "null", "waitlevel", "lockbottom",

                        "module", "external",

                        "predicate", "function", "free", "send", "receive",

                        "ite", "fold", "unfold", "unfolding", "in", "forall", "exists", 

@@ -406,7 +410,7 @@ class Parser extends StandardTokenParsers {
     | "false" ^^^ BoolLiteral(false)

     | "true" ^^^ BoolLiteral(true)

     | "null" ^^^ NullLiteral()

-    | "maxlock" ^^^ MaxLockLiteral()

+    | "waitlevel" ^^^ MaxLockLiteral()

     | "lockbottom" ^^^ LockBottomLiteral()

     | "this" ^^^ ExplicitThisExpr()

     | "result" ^^^ Result()

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index a97a04f9..dea0f2d5 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -199,7 +199,7 @@ object PrintProgram {
     case IntLiteral(n) => print(n)

     case BoolLiteral(b) => print(b)

     case NullLiteral() => print("null")

-    case MaxLockLiteral() => print("maxlock")

+    case MaxLockLiteral() => print("waitlevel")

     case LockBottomLiteral() => print("lockbottom")

     case _:ThisExpr => print("this")

     case _:Result => print("result")

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 9e8e5b4a..4ce95b3e 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -7,1061 +7,1061 @@ import scala.util.parsing.input.Position
 import scala.util.parsing.input.Positional

 

 object Resolver {

-  sealed abstract class ResolverOutcome

-  case class Success extends ResolverOutcome

-  case class Errors(ss: List[(Position,String)]) extends ResolverOutcome

+ sealed abstract class ResolverOutcome

+ case class Success extends ResolverOutcome

+ case class Errors(ss: List[(Position,String)]) extends ResolverOutcome

 

-  var seqClasses = Map[String, SeqClass]();

+ var seqClasses = Map[String, SeqClass]();

 

-  class ProgramContext(decls: Map[String,TopLevelDecl], currentClass: Class) {

-    val Decls = decls

-    val CurrentClass = currentClass

-    var currentMember = null: Member;

-    def CurrentMember = currentMember: Member;  

-    var errors: List[(Position,String)] = Nil

-    def Error(pos: Position, msg: String) {

-      errors = errors + (pos, msg)

-    }

-    def AddVariable(v: Variable): ProgramContext = {

-      new LProgramContext(v, this);

-    }

-    def LookupVariable(id: String): Option[Variable] = None

-    def IsVariablePresent(vr: Variable): boolean = false

+ class ProgramContext(decls: Map[String,TopLevelDecl], currentClass: Class) {

+   val Decls = decls

+   val CurrentClass = currentClass

+   var currentMember = null: Member;

+   def CurrentMember = currentMember: Member;  

+   var errors: List[(Position,String)] = Nil

+   def Error(pos: Position, msg: String) {

+     errors = errors + (pos, msg)

+   }

+   def AddVariable(v: Variable): ProgramContext = {

+     new LProgramContext(v, this);

+   }

+   def LookupVariable(id: String): Option[Variable] = None

+   def IsVariablePresent(vr: Variable): boolean = false

 

-    private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Decls, parent.CurrentClass) {

-      override def Error(pos: Position, msg: String) = parent.Error(pos, msg)

-      override def LookupVariable(id: String): Option[Variable] = {

-        if (id == v.id) Some(v) else parent.LookupVariable(id)

-      }

-      override def IsVariablePresent(vr: Variable): boolean = {

-        if (vr == v) true else parent.IsVariablePresent(vr)

-      }

-      override def CurrentMember() = {

-        parent.CurrentMember

-      }

-    }

-  }

+   private class LProgramContext(v: Variable, parent: ProgramContext) extends ProgramContext(parent.Decls, parent.CurrentClass) {

+     override def Error(pos: Position, msg: String) = parent.Error(pos, msg)

+     override def LookupVariable(id: String): Option[Variable] = {

+       if (id == v.id) Some(v) else parent.LookupVariable(id)

+     }

+     override def IsVariablePresent(vr: Variable): boolean = {

+       if (vr == v) true else parent.IsVariablePresent(vr)

+     }

+     override def CurrentMember() = {

+       parent.CurrentMember

+     }

+   }

+ }

 

-  def Resolve(prog: List[TopLevelDecl]): ResolverOutcome = {

-    // register the channels as well as the classes and their members

-    var decls = Map[String,TopLevelDecl]()

-    for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {

-      if (decls contains decl.id) {

-        return Errors(List((decl.pos, "duplicate class/channel name: " + decl.id)))

-      } else {

-        decl match {

-          case cl: Class =>

-            for (m <- cl.members) m match {

-              case _:MonitorInvariant =>

-              case m: NamedMember =>

-                m.Parent = cl

-                if (cl.mm contains m.Id) {

-                  return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id)))

-                } else {

-                  cl.mm = cl.mm + (m.Id -> m)

-                }

-            }

-          case ch: Channel =>

-        }

-        decls = decls + (decl.id -> decl)

-      }

-    }

-    var errors = List[(Position,String)]()

+ def Resolve(prog: List[TopLevelDecl]): ResolverOutcome = {

+   // register the channels as well as the classes and their members

+   var decls = Map[String,TopLevelDecl]()

+   for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {

+     if (decls contains decl.id) {

+       return Errors(List((decl.pos, "duplicate class/channel name: " + decl.id)))

+     } else {

+       decl match {

+         case cl: Class =>

+           for (m <- cl.members) m match {

+             case _:MonitorInvariant =>

+             case m: NamedMember =>

+               m.Parent = cl

+               if (cl.mm contains m.Id) {

+                 return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id)))

+               } else {

+                 cl.mm = cl.mm + (m.Id -> m)

+               }

+           }

+         case ch: Channel =>

+       }

+       decls = decls + (decl.id -> decl)

+     }

+   }

+   var errors = List[(Position,String)]()

 

-    // resolve types of members

-    val contextNoCurrentClass = new ProgramContext(decls, null)

-    for (decl <- prog) decl match {

-      case ch: Channel =>

-        for (v <- ch.parameters) {

-          ResolveType(v.t, contextNoCurrentClass)

-	    }

-      case cl: Class =>

-        for (m <- cl.asInstanceOf[Class].members) m match {

-          case _:MonitorInvariant =>

-          case Field(id,t) =>

-            ResolveType(t, contextNoCurrentClass)

-          case Method(id, ins, outs, spec, body) =>

-            for (v <- ins ++ outs) {

-              ResolveType(v.t, contextNoCurrentClass)

-            }

-          case _:Condition =>

-          case _:Predicate =>

-          case Function(id, ins, out, specs, definition) => 

-            for (v <- ins) {

-              ResolveType(v.t, contextNoCurrentClass)

-            }

-            ResolveType(out, contextNoCurrentClass)

+   // resolve types of members

+   val contextNoCurrentClass = new ProgramContext(decls, null)

+   for (decl <- prog) decl match {

+     case ch: Channel =>

+       for (v <- ch.parameters) {

+         ResolveType(v.t, contextNoCurrentClass)

         }

-    }

-    errors = errors ++ contextNoCurrentClass.errors;

+     case cl: Class =>

+       for (m <- cl.asInstanceOf[Class].members) m match {

+         case _:MonitorInvariant =>

+         case Field(id,t) =>

+           ResolveType(t, contextNoCurrentClass)

+         case Method(id, ins, outs, spec, body) =>

+           for (v <- ins ++ outs) {

+             ResolveType(v.t, contextNoCurrentClass)

+           }

+         case _:Condition =>

+         case _:Predicate =>

+         case Function(id, ins, out, specs, definition) => 

+           for (v <- ins) {

+             ResolveType(v.t, contextNoCurrentClass)

+           }

+           ResolveType(out, contextNoCurrentClass)

+       }

+   }

+   errors = errors ++ contextNoCurrentClass.errors;

 

-    // now, resolve and typecheck all

-    //  * Field types and Method formal-parameter types

-    //  * Assign, FieldUpdate, and Call statements

-    //  * VariableExpr and FieldSelect expressions

-    for (decl <- prog) decl match {

-      case ch: Channel =>

-	    val context = new ProgramContext(decls, ChannelClass(ch))

-        var ctx = context

-        for (v <- ch.parameters) {

-          ctx = ctx.AddVariable(v)

-        }

-        ResolveExpr(ch.where, ctx, false, true)(false)

-		errors = errors ++ context.errors

-      case cl: Class =>

-        val context = new ProgramContext(decls, cl)

-        for (m <- cl.members) {

-          context.currentMember = m;

-          m match {

-            case MonitorInvariant(e) =>

-              ResolveExpr(e, context, true, true)(true)

-              if (!e.typ.IsBool) context.Error(m.pos, "monitor invariant requires a boolean expression (found " + e.typ.FullName + ")")

-            case _:Field => // nothing more to do

-            case m@Method(id, ins, outs, spec, body) =>

-              var ctx = context

-              for (v <- ins ++ outs) {

-                ctx = ctx.AddVariable(v)

-              }

-              spec foreach {

-                case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)

-                case Postcondition(e) => ResolveExpr(e, ctx, true, true)(false)

-                case lc@LockChange(ee) => 

-                if(m.id.equals("run")) context.Error(lc.pos, "lockchange not allowed on method run") 

-                ee foreach (e => ResolveExpr(e, ctx, true, false)(false))

-              }

-              ResolveStmt(BlockStmt(body), ctx)

-            case Condition(id, None) =>

-            case c@Condition(id, Some(e)) =>

-              ResolveExpr(e, context, false, true)(false)

-              if (!e.typ.IsBool) context.Error(c.pos, "where clause requires a boolean expression (found " + e.typ.FullName + ")")

-            case p@Predicate(id, e) =>

-              var ctx = context;

-              ResolveExpr(e, ctx, false, true)(true);

-              if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")")

-            case f@Function(id, ins, out, spec, e) =>

-              var ctx = context

-              for (v <- ins) {

-                ctx = ctx.AddVariable(v)

-              }

-	      // TODO: disallow credit(...) expressions in function specifications

-              spec foreach {

-                case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)

-                case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false)

-                case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function") 

-              }

-              ResolveExpr(e, ctx, false, false)(false)

-              if(! canAssign(out.typ, e.typ)) context.Error(e.pos, "function body does not match declared type (expected: " + out.FullName + ", found: " + e.typ.FullName + ")")

-          }

-        }

+   // now, resolve and typecheck all

+   //  * Field types and Method formal-parameter types

+   //  * Assign, FieldUpdate, and Call statements

+   //  * VariableExpr and FieldSelect expressions

+   for (decl <- prog) decl match {

+     case ch: Channel =>

+        val context = new ProgramContext(decls, ChannelClass(ch))

+       var ctx = context

+       for (v <- ch.parameters) {

+         ctx = ctx.AddVariable(v)

+       }

+       ResolveExpr(ch.where, ctx, false, true)(false)

         errors = errors ++ context.errors

-    }

+     case cl: Class =>

+       val context = new ProgramContext(decls, cl)

+       for (m <- cl.members) {

+         context.currentMember = m;

+         m match {

+           case MonitorInvariant(e) =>

+             ResolveExpr(e, context, true, true)(true)

+             if (!e.typ.IsBool) context.Error(m.pos, "monitor invariant requires a boolean expression (found " + e.typ.FullName + ")")

+           case _:Field => // nothing more to do

+           case m@Method(id, ins, outs, spec, body) =>

+             var ctx = context

+             for (v <- ins ++ outs) {

+               ctx = ctx.AddVariable(v)

+             }

+             spec foreach {

+               case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)

+               case Postcondition(e) => ResolveExpr(e, ctx, true, true)(false)

+               case lc@LockChange(ee) => 

+               if(m.id.equals("run")) context.Error(lc.pos, "lockchange not allowed on method run") 

+               ee foreach (e => ResolveExpr(e, ctx, true, false)(false))

+             }

+             ResolveStmt(BlockStmt(body), ctx)

+           case Condition(id, None) =>

+           case c@Condition(id, Some(e)) =>

+             ResolveExpr(e, context, false, true)(false)

+             if (!e.typ.IsBool) context.Error(c.pos, "where clause requires a boolean expression (found " + e.typ.FullName + ")")

+           case p@Predicate(id, e) =>

+             var ctx = context;

+             ResolveExpr(e, ctx, false, true)(true);

+             if(!e.typ.IsBool) context.Error(e.pos, "predicate requires a boolean expression (found " + e.typ.FullName + ")")

+           case f@Function(id, ins, out, spec, e) =>

+             var ctx = context

+             for (v <- ins) {

+               ctx = ctx.AddVariable(v)

+             }

+          // TODO: disallow credit(...) expressions in function specifications

+             spec foreach {

+               case Precondition(e) => ResolveExpr(e, ctx, false, true)(false)

+               case pc@Postcondition(e) => assert(ctx.CurrentMember != null); ResolveExpr(e, ctx, false, true)(false)

+               case lc@LockChange(ee) => context.Error(lc.pos, "lockchange not allowed on function") 

+             }

+             ResolveExpr(e, ctx, false, false)(false)

+             if(! canAssign(out.typ, e.typ)) context.Error(e.pos, "function body does not match declared type (expected: " + out.FullName + ", found: " + e.typ.FullName + ")")

+         }

+       }

+       errors = errors ++ context.errors

+   }

 

-    if (errors.length == 0) {

-      Success()

-    } else {

-      Errors(errors)

-    }

-  }

+   if (errors.length == 0) {

+     Success()

+   } else {

+     Errors(errors)

+   }

+ }

 

-  def ResolveType(t: Type, context: ProgramContext): unit = {

-      for(p <- t.params){

-        ResolveType(p, context);

-      }

-      if(t.isInstanceOf[TokenType]){

-        val tt = t.asInstanceOf[TokenType];

-        ResolveType(tt.C, context);

-        if(! tt.C.typ.IsNormalClass) context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " is not a user-defined class.");

-        tt.C.typ.LookupMember(tt.m) match {

-          case Some(m: Method) => val tc = TokenClass(tt.C, tt.m); tc.method = m; tt.typ = tc;

-          case _ => context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " does not declare a method " + tt.m + ".");

-        }

-        return;

-      }

-      if (context.Decls contains t.FullName) {

-        context.Decls(t.FullName) match {

-          case cl: Class => t.typ = cl

-          case ch: Channel => t.typ = ChannelClass(ch)

-          case _ =>

-            context.Error(t.pos, "Invalid class: " + t.FullName + " does not denote a class")

-            t.typ = IntClass

-        }

-      } else {

-        if(seqClasses.contains(t.FullName)) {

-          t.typ = seqClasses(t.FullName)

-        } else if(t.id.equals("seq") && t.params.length == 1) {

-          val seqt = new SeqClass(t.params(0).typ);

-          seqClasses = seqClasses + ((seqt.FullName, seqt));

-          t.typ = seqt;

-        } else {

-          context.Error(t.pos, "undeclared type " + t.FullName)

-          t.typ = IntClass

-        }

-      }

-  }

+ def ResolveType(t: Type, context: ProgramContext): unit = {

+     for(p <- t.params){

+       ResolveType(p, context);

+     }

+     if(t.isInstanceOf[TokenType]){

+       val tt = t.asInstanceOf[TokenType];

+       ResolveType(tt.C, context);

+       if(! tt.C.typ.IsNormalClass) context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " is not a user-defined class.");

+       tt.C.typ.LookupMember(tt.m) match {

+         case Some(m: Method) => val tc = TokenClass(tt.C, tt.m); tc.method = m; tt.typ = tc;

+         case _ => context.Error(t.pos, "Invalid token type. " + tt.C.FullName + " does not declare a method " + tt.m + ".");

+       }

+       return;

+     }

+     if (context.Decls contains t.FullName) {

+       context.Decls(t.FullName) match {

+         case cl: Class => t.typ = cl

+         case ch: Channel => t.typ = ChannelClass(ch)

+         case _ =>

+           context.Error(t.pos, "Invalid class: " + t.FullName + " does not denote a class")

+           t.typ = IntClass

+       }

+     } else {

+       if(seqClasses.contains(t.FullName)) {

+         t.typ = seqClasses(t.FullName)

+       } else if(t.id.equals("seq") && t.params.length == 1) {

+         val seqt = new SeqClass(t.params(0).typ);

+         seqClasses = seqClasses + ((seqt.FullName, seqt));

+         t.typ = seqt;

+       } else {

+         context.Error(t.pos, "undeclared type " + t.FullName)

+         t.typ = IntClass

+       }

+     }

+ }

 

-  def getSeqType(param: Class, context: ProgramContext): Class = {

-    if(seqClasses.contains("seq<" + param.FullName + ">")) {

-      seqClasses("seq<" + param.FullName + ">")

-    } else {

-      val seqt = new SeqClass(param);

-      seqClasses = seqClasses + ((seqt.FullName, seqt));

-      seqt

-    }

-  }

+ def getSeqType(param: Class, context: ProgramContext): Class = {

+   if(seqClasses.contains("seq<" + param.FullName + ">")) {

+     seqClasses("seq<" + param.FullName + ">")

+   } else {

+     val seqt = new SeqClass(param);

+     seqClasses = seqClasses + ((seqt.FullName, seqt));

+     seqt

+   }

+ }

 

-  def ResolveStmt(s: Statement, context: ProgramContext): unit = s match {

-    case Assert(e) =>

-      ResolveExpr(e, context, true, true)(false)

-      if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")")

-    case Assume(e) =>

-      ResolveExpr(e, context, false, false)(false)  // assume expressions remain at run-time, so OLD is not allowed

-      if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")

-      CheckNoGhost(e, context)

-    case BlockStmt(ss) =>

-      var ctx = context

-      for (s <- ss) s match {

-        case l @ LocalVar(id, t, c, g, rhs) =>

-          ResolveType(l.v.t, ctx)

-          val oldCtx = ctx

-          ctx = ctx.AddVariable(l.v)

-          rhs match {

-            case None =>

-            case Some(rhs) =>

-              val lhs = VariableExpr(id)

-              lhs.pos = l.pos;

-              ResolveExpr(lhs, ctx, false, false)(false)

-              ResolveAssign(lhs, rhs, oldCtx)

-          }

-        case c: CallAsync =>

-          ResolveStmt(c, ctx)

-          if (c.local != null) {

-            ctx = ctx.AddVariable(c.local)

-          }

-        case c: Call =>

-          ResolveStmt(c, ctx)

-          for (v <- c.locals) { ctx = ctx.AddVariable(v) } 

-        case r: Receive =>

-          ResolveStmt(r, ctx)

-          for (v <- r.locals) { ctx = ctx.AddVariable(v) } 

-        case s =>

-          ResolveStmt(s, ctx)

-      }

-    case IfStmt(guard, thn, els) =>

-      ResolveExpr(guard, context, false, false)(false)

-      if (!guard.typ.IsBool) context.Error(guard.pos, "if statement requires a boolean guard (found " + guard.typ.FullName + ")")

-      CheckNoGhost(guard, context)

-      ResolveStmt(thn, context)

-      els match { case None => case Some(s) => ResolveStmt(s, context) }

-    case w@ WhileStmt(guard, invs, lkch, body) =>

-      ResolveExpr(guard, context, false, false)(false)

-      if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")")

-      CheckNoGhost(guard, context)

-      for (inv <- invs) {

-        ResolveExpr(inv, context, true, true)(false)

-        if (!inv.typ.IsBool) context.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")

-      }

-      for (l <- lkch) {

-        ResolveExpr(l, context, true, false)(false)

-        if (!l.typ.IsRef) context.Error(l.pos, "lockchange expression must be reference (found " + l.typ.FullName + ")")

-      }

-      ResolveStmt(body, context)

-      w.LoopTargets = ComputeLoopTargets(body) filter context.IsVariablePresent

-    case Assign(lhs, rhs) => 

-      ResolveExpr(lhs, context, false, false)(false)

-      ResolveAssign(lhs, rhs, context)

-      if (lhs.v != null && lhs.v.IsImmutable) {

-        if (lhs.v.IsGhost)

-          CheckNoGhost(rhs, context)

-        else

-          context.Error(lhs.pos, "cannot assign to immutable variable " + lhs.v.id)

-      }

-    case fu@FieldUpdate(lhs, rhs) =>

-      ResolveExpr(lhs, context, false, false)(false)

-      if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(lhs.e, context)

-      if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id)

-      ResolveExpr(rhs, context, false, false)(false)

-      if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)

-      if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context)

-    case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")

-    case c @ Call(declaresLocal, lhs, obj, id, args) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }

-      // lookup method

-      var typ: Class = IntClass

-      obj.typ.LookupMember(id) match {

-        case None =>

-          context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)

-        case Some(m: Method) =>

-          c.m = m

-          if (args.length != m.ins.length)

-            context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +

-                          " (" + args.length + " instead of " + m.ins.length + ")")

-          else {

-            for((actual, formal) <- args zip m.ins){

-              if(! canAssign(formal.t.typ, actual.typ))

-                context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

-            }

-          }     

-          if (lhs.length != m.outs.length)

-            context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id +

-                          " (" + lhs.length + " instead of " + m.outs.length + ")")

-          else

-            c.locals = ResolveLHS(declaresLocal, lhs, m.outs, context)

-        case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)

-      }

-    case Install(obj, lowerBounds, upperBounds) =>

-      ResolveExpr(obj, context, false, false)(false)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in reorder statement must be of a reference type (found " + obj.typ.FullName + ")")

-      if (obj.typ.IsChannel) context.Error(obj.pos, "object in reorder statement must not be a channel (found " + obj.typ.FullName + ")")

-      ResolveBounds(lowerBounds, upperBounds, context, "install")

-    case Share(obj, lowerBounds, upperBounds) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in share statement must be of a reference type (found " + obj.typ.FullName + ")")

-      if (obj.typ.IsChannel) context.Error(obj.pos, "object in share statement must not be a channel (found " + obj.typ.FullName + ")")

-      ResolveBounds(lowerBounds, upperBounds, context, "share")

-    case Unshare(obj) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in unshare statement must be of a reference type (found " + obj.typ.FullName + ")")

-      if (obj.typ.IsChannel) context.Error(obj.pos, "object in unshare statement must not be a channel (found " + obj.typ.FullName + ")")

-    case Acquire(obj) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in acquire statement must be of a reference type (found " + obj.typ.FullName + ")")

-    case Release(obj) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in release statement must be of a reference type (found " + obj.typ.FullName + ")")

-    case RdAcquire(obj) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd acquire statement must be of a reference type (found " + obj.typ.FullName + ")")

-    case RdRelease(obj) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd release statement must be of a reference type (found " + obj.typ.FullName + ")")

-    case Lock(obj, b, rdLock) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) {

-        val sname = if (rdLock) "rd lock" else "lock";

-        context.Error(obj.pos, "object in " + sname + " statement must be of a reference type (found " + obj.typ.FullName + ")")

-                                       

-      }

-      ResolveStmt(b, context)

-    case Downgrade(obj) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in downgrade statement must be of a reference type (found " + obj.typ.FullName + ")")

-    case Free(obj) =>

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      if (!obj.typ.IsRef) context.Error(obj.pos, "object in free statement must be of a reference type (found " + obj.typ.FullName + ")")

-    case fld@Fold(e) =>

-      ResolveExpr(e, context, false, true)(false);

-      CheckNoGhost(e, context);

-      if(!e.getMemberAccess.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.")

-    case ufld@Unfold(e) =>

-      ResolveExpr(e, context, false, true)(false);

-      CheckNoGhost(e, context);

-      if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")

-    case c@CallAsync(declaresLocal, token, obj, id, args) => 

-      // resolve receiver

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      // resolve arguments

-      args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }

-      // lookup method

-      var typ: Class = IntClass

-      obj.typ.LookupMember(id) match {

-        case None =>

-          context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)

-        case Some(m: Method) =>

-          c.m = m

-          if (args.length != m.ins.length)

-            context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +

-                          " (" + args.length + " instead of " + m.ins.length + ")")

-          else {

-            for((actual, formal) <- args zip m.ins){

-              if(! canAssign(formal.t.typ, actual.typ))

-                context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

-            }

-          }

-        case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)

-      }

-      // resolve the token

-      if (declaresLocal) {

-        c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))

-        ResolveType(c.local.t, context)

-        token.Resolve(c.local)

-      } else if (token != null) {

-        ResolveExpr(token, context, false, false)(false)

-        if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id)))

-          context.Error(token.pos, "wrong token type")

-      }

-    case jn@JoinAsync(lhs, token) =>

-      // resolve the assignees

-      var vars = Set[Variable]()

-      for (v <- lhs) {

-        ResolveExpr(v, context, false, false)(false)

-        if (v.v != null) {

-          if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")

-          if (vars contains v.v) {

-            context.Error(v.pos, "duplicate actual out-parameter: " + v.id)

-          } else {

-            vars = vars + v.v

-          }

-        }

-      }

-      // resolve the token

-      ResolveExpr(token, context, false, false)(false);

-      if(token.typ == null || ! token.typ.IsToken || ! token.typ.isInstanceOf[TokenClass] || token.typ.asInstanceOf[TokenClass].method == null)

-        context.Error(token.pos, "the first argument of a join async must be a token")

-      else {

-        val m = token.typ.asInstanceOf[TokenClass].method;

-        jn.m = m

-        if (lhs.length != m.outs.length)

-          context.Error(jn.pos, "wrong number of actual out-parameters in join async of " + m.FullName +

+ def ResolveStmt(s: Statement, context: ProgramContext): unit = s match {

+   case Assert(e) =>

+     ResolveExpr(e, context, true, true)(false)

+     if (!e.typ.IsBool) context.Error(e.pos, "assert statement requires a boolean expression (found " + e.typ.FullName + ")")

+   case Assume(e) =>

+     ResolveExpr(e, context, false, false)(false)  // assume expressions remain at run-time, so OLD is not allowed

+     if (!e.typ.IsBool) context.Error(e.pos, "assume statement requires a boolean expression (found " + e.typ.FullName + ")")

+     CheckNoGhost(e, context)

+   case BlockStmt(ss) =>

+     var ctx = context

+     for (s <- ss) s match {

+       case l @ LocalVar(id, t, c, g, rhs) =>

+         ResolveType(l.v.t, ctx)

+         val oldCtx = ctx

+         ctx = ctx.AddVariable(l.v)

+         rhs match {

+           case None =>

+           case Some(rhs) =>

+             val lhs = VariableExpr(id)

+             lhs.pos = l.pos;

+             ResolveExpr(lhs, ctx, false, false)(false)

+             ResolveAssign(lhs, rhs, oldCtx)

+         }

+       case c: CallAsync =>

+         ResolveStmt(c, ctx)

+         if (c.local != null) {

+           ctx = ctx.AddVariable(c.local)

+         }

+       case c: Call =>

+         ResolveStmt(c, ctx)

+         for (v <- c.locals) { ctx = ctx.AddVariable(v) } 

+       case r: Receive =>

+         ResolveStmt(r, ctx)

+         for (v <- r.locals) { ctx = ctx.AddVariable(v) } 

+       case s =>

+         ResolveStmt(s, ctx)

+     }

+   case IfStmt(guard, thn, els) =>

+     ResolveExpr(guard, context, false, false)(false)

+     if (!guard.typ.IsBool) context.Error(guard.pos, "if statement requires a boolean guard (found " + guard.typ.FullName + ")")

+     CheckNoGhost(guard, context)

+     ResolveStmt(thn, context)

+     els match { case None => case Some(s) => ResolveStmt(s, context) }

+   case w@ WhileStmt(guard, invs, lkch, body) =>

+     ResolveExpr(guard, context, false, false)(false)

+     if (!guard.typ.IsBool) context.Error(guard.pos, "while statement requires a boolean guard (found " + guard.typ.FullName + ")")

+     CheckNoGhost(guard, context)

+     for (inv <- invs) {

+       ResolveExpr(inv, context, true, true)(false)

+       if (!inv.typ.IsBool) context.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")

+     }

+     for (l <- lkch) {

+       ResolveExpr(l, context, true, false)(false)

+       if (!l.typ.IsRef) context.Error(l.pos, "lockchange expression must be reference (found " + l.typ.FullName + ")")

+     }

+     ResolveStmt(body, context)

+     w.LoopTargets = ComputeLoopTargets(body) filter context.IsVariablePresent

+   case Assign(lhs, rhs) => 

+     ResolveExpr(lhs, context, false, false)(false)

+     ResolveAssign(lhs, rhs, context)

+     if (lhs.v != null && lhs.v.IsImmutable) {

+       if (lhs.v.IsGhost)

+         CheckNoGhost(rhs, context)

+       else

+         context.Error(lhs.pos, "cannot assign to immutable variable " + lhs.v.id)

+     }

+   case fu@FieldUpdate(lhs, rhs) =>

+     ResolveExpr(lhs, context, false, false)(false)

+     if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(lhs.e, context)

+     if (! lhs.isPredicate && lhs.f.isInstanceOf[SpecialField]) context.Error(lhs.pos, "cannot assign directly to special field: " + lhs.id)

+     ResolveExpr(rhs, context, false, false)(false)

+     if (! lhs.isPredicate && !canAssign(lhs.typ, rhs.typ)) context.Error(fu.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)

+     if (! lhs.isPredicate && lhs.f != null && !lhs.f.IsGhost) CheckNoGhost(rhs, context)

+   case lv:LocalVar => throw new Exception("unexpected LocalVar; should have been handled in BlockStmt above")

+   case c @ Call(declaresLocal, lhs, obj, id, args) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }

+     // lookup method

+     var typ: Class = IntClass

+     obj.typ.LookupMember(id) match {

+       case None =>

+         context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)

+       case Some(m: Method) =>

+         c.m = m

+         if (args.length != m.ins.length)

+           context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +

+                         " (" + args.length + " instead of " + m.ins.length + ")")

+         else {

+           for((actual, formal) <- args zip m.ins){

+             if(! canAssign(formal.t.typ, actual.typ))

+               context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+           }

+         }     

+         if (lhs.length != m.outs.length)

+           context.Error(c.pos, "wrong number of actual out-parameters in call to " + obj.typ.FullName + "." + id +

                          " (" + lhs.length + " instead of " + m.outs.length + ")")

-        else {

-          for((out, l) <- m.outs zip lhs){

-            if(! canAssign(l.typ, out.t.typ))

-              context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")

-          }

-        }

-      

-      }

-    case w@Wait(obj, id) =>

-      // resolve receiver

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      // lookup condition

-      obj.typ.LookupMember(id) match {

-        case None =>

-          context.Error(w.pos, "wait on undeclared member " + id + " in class " + obj.typ.FullName)

-        case Some(c: Condition) => w.c = c

-        case _ =>

-          context.Error(w.pos, "wait expression does not denote a condition: " + obj.typ.FullName + "." + id)

-      }

-    case s@Signal(obj, id, all) =>

-      // resolve receiver

-      ResolveExpr(obj, context, false, false)(false)

-      CheckNoGhost(obj, context)

-      // lookup condition

-      obj.typ.LookupMember(id) match {

-        case None =>

-          context.Error(s.pos, "signal on undeclared member " + id + " in class " + obj.typ.FullName)

-        case Some(c: Condition) => s.c = c

-        case _ =>

-          context.Error(s.pos, "signal expression does not denote a condition: " + obj.typ.FullName + "." + id)

-      }

-    case s@Send(ch, args) =>

-      ResolveExpr(ch, context, false, false)(false)

-      CheckNoGhost(ch, context)

-      args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }

-      // match types of arguments

-      ch.typ match {

-        case ChannelClass(channel) =>

-          if (args.length != channel.parameters.length)

-            context.Error(s.pos, "wrong number of actual in-parameters in send for channel type " + ch.typ.FullName +

-                          " (" + args.length + " instead of " + channel.parameters.length + ")")

-          else {

-            for ((actual, formal) <- args zip channel.parameters) {

-              if (! canAssign(formal.t.typ, actual.typ))

-                context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

-            }

-          }

-        case _ => context.Error(s.pos, "send expression (which has type " + ch.typ.FullName + ") does not denote a channel")

-      }

-    case r@Receive(declaresLocal, ch, outs) =>

-      ResolveExpr(ch, context, false, false)(false)

-      CheckNoGhost(ch, context)

-      // match types of arguments

-      ch.typ match {

-        case ChannelClass(channel) =>

-          if (outs.length != channel.parameters.length)

-            context.Error(r.pos, "wrong number of actual out-parameters in receive for channel type " + ch.typ.FullName +

-                          " (" + outs.length + " instead of " + channel.parameters.length + ")")

-          else

-            r.locals = ResolveLHS(declaresLocal, outs, channel.parameters, context)

-        case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel")

-      }

-  }

+         else

+           c.locals = ResolveLHS(declaresLocal, lhs, m.outs, context)

+       case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)

+     }

+   case Install(obj, lowerBounds, upperBounds) =>

+     ResolveExpr(obj, context, false, false)(false)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in reorder statement must be of a reference type (found " + obj.typ.FullName + ")")

+     if (obj.typ.IsChannel) context.Error(obj.pos, "object in reorder statement must not be a channel (found " + obj.typ.FullName + ")")

+     ResolveBounds(lowerBounds, upperBounds, context, "install")

+   case Share(obj, lowerBounds, upperBounds) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in share statement must be of a reference type (found " + obj.typ.FullName + ")")

+     if (obj.typ.IsChannel) context.Error(obj.pos, "object in share statement must not be a channel (found " + obj.typ.FullName + ")")

+     ResolveBounds(lowerBounds, upperBounds, context, "share")

+   case Unshare(obj) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in unshare statement must be of a reference type (found " + obj.typ.FullName + ")")

+     if (obj.typ.IsChannel) context.Error(obj.pos, "object in unshare statement must not be a channel (found " + obj.typ.FullName + ")")

+   case Acquire(obj) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in acquire statement must be of a reference type (found " + obj.typ.FullName + ")")

+   case Release(obj) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in release statement must be of a reference type (found " + obj.typ.FullName + ")")

+   case RdAcquire(obj) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd acquire statement must be of a reference type (found " + obj.typ.FullName + ")")

+   case RdRelease(obj) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in rd release statement must be of a reference type (found " + obj.typ.FullName + ")")

+   case Lock(obj, b, rdLock) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) {

+       val sname = if (rdLock) "rd lock" else "lock";

+       context.Error(obj.pos, "object in " + sname + " statement must be of a reference type (found " + obj.typ.FullName + ")")

+                                      

+     }

+     ResolveStmt(b, context)

+   case Downgrade(obj) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in downgrade statement must be of a reference type (found " + obj.typ.FullName + ")")

+   case Free(obj) =>

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     if (!obj.typ.IsRef) context.Error(obj.pos, "object in free statement must be of a reference type (found " + obj.typ.FullName + ")")

+   case fld@Fold(e) =>

+     ResolveExpr(e, context, false, true)(false);

+     CheckNoGhost(e, context);

+     if(!e.getMemberAccess.isPredicate) context.Error(fld.pos, "Fold can only be applied to predicates.")

+   case ufld@Unfold(e) =>

+     ResolveExpr(e, context, false, true)(false);

+     CheckNoGhost(e, context);

+     if(!e.getMemberAccess.isPredicate) context.Error(ufld.pos, "Unfold can only be applied to predicates.")

+   case c@CallAsync(declaresLocal, token, obj, id, args) => 

+     // resolve receiver

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     // resolve arguments

+     args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }

+     // lookup method

+     var typ: Class = IntClass

+     obj.typ.LookupMember(id) match {

+       case None =>

+         context.Error(c.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)

+       case Some(m: Method) =>

+         c.m = m

+         if (args.length != m.ins.length)

+           context.Error(c.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +

+                         " (" + args.length + " instead of " + m.ins.length + ")")

+         else {

+           for((actual, formal) <- args zip m.ins){

+             if(! canAssign(formal.t.typ, actual.typ))

+               context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+           }

+         }

+       case _ => context.Error(c.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)

+     }

+     // resolve the token

+     if (declaresLocal) {

+       c.local = new Variable(token.id, TokenType(new Type(obj.typ), id))

+       ResolveType(c.local.t, context)

+       token.Resolve(c.local)

+     } else if (token != null) {

+       ResolveExpr(token, context, false, false)(false)

+       if(! canAssign(token.typ, TokenClass(new Type(obj.typ), id)))

+         context.Error(token.pos, "wrong token type")

+     }

+   case jn@JoinAsync(lhs, token) =>

+     // resolve the assignees

+     var vars = Set[Variable]()

+     for (v <- lhs) {

+       ResolveExpr(v, context, false, false)(false)

+       if (v.v != null) {

+         if (v.v.IsImmutable) context.Error(v.pos, "cannot use immutable variable " + v.id + " as actual out-parameter")

+         if (vars contains v.v) {

+           context.Error(v.pos, "duplicate actual out-parameter: " + v.id)

+         } else {

+           vars = vars + v.v

+         }

+       }

+     }

+     // resolve the token

+     ResolveExpr(token, context, false, false)(false);

+     if(token.typ == null || ! token.typ.IsToken || ! token.typ.isInstanceOf[TokenClass] || token.typ.asInstanceOf[TokenClass].method == null)

+       context.Error(token.pos, "the first argument of a join async must be a token")

+     else {

+       val m = token.typ.asInstanceOf[TokenClass].method;

+       jn.m = m

+       if (lhs.length != m.outs.length)

+         context.Error(jn.pos, "wrong number of actual out-parameters in join async of " + m.FullName +

+                        " (" + lhs.length + " instead of " + m.outs.length + ")")

+       else {

+         for((out, l) <- m.outs zip lhs){

+           if(! canAssign(l.typ, out.t.typ))

+             context.Error(l.pos, "the out parameter cannot be assigned to the lhs (expected: " + l.typ.FullName + ", found: " + out.t.FullName + ")")

+         }

+       }

+     

+     }

+   case w@Wait(obj, id) =>

+     // resolve receiver

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     // lookup condition

+     obj.typ.LookupMember(id) match {

+       case None =>

+         context.Error(w.pos, "wait on undeclared member " + id + " in class " + obj.typ.FullName)

+       case Some(c: Condition) => w.c = c

+       case _ =>

+         context.Error(w.pos, "wait expression does not denote a condition: " + obj.typ.FullName + "." + id)

+     }

+   case s@Signal(obj, id, all) =>

+     // resolve receiver

+     ResolveExpr(obj, context, false, false)(false)

+     CheckNoGhost(obj, context)

+     // lookup condition

+     obj.typ.LookupMember(id) match {

+       case None =>

+         context.Error(s.pos, "signal on undeclared member " + id + " in class " + obj.typ.FullName)

+       case Some(c: Condition) => s.c = c

+       case _ =>

+         context.Error(s.pos, "signal expression does not denote a condition: " + obj.typ.FullName + "." + id)

+     }

+   case s@Send(ch, args) =>

+     ResolveExpr(ch, context, false, false)(false)

+     CheckNoGhost(ch, context)

+     args foreach { a => ResolveExpr(a, context, false, false)(false); CheckNoGhost(a, context) }

+     // match types of arguments

+     ch.typ match {

+       case ChannelClass(channel) =>

+         if (args.length != channel.parameters.length)

+           context.Error(s.pos, "wrong number of actual in-parameters in send for channel type " + ch.typ.FullName +

+                         " (" + args.length + " instead of " + channel.parameters.length + ")")

+         else {

+           for ((actual, formal) <- args zip channel.parameters) {

+             if (! canAssign(formal.t.typ, actual.typ))

+               context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+           }

+         }

+       case _ => context.Error(s.pos, "send expression (which has type " + ch.typ.FullName + ") does not denote a channel")

+     }

+   case r@Receive(declaresLocal, ch, outs) =>

+     ResolveExpr(ch, context, false, false)(false)

+     CheckNoGhost(ch, context)

+     // match types of arguments

+     ch.typ match {

+       case ChannelClass(channel) =>

+         if (outs.length != channel.parameters.length)

+           context.Error(r.pos, "wrong number of actual out-parameters in receive for channel type " + ch.typ.FullName +

+                         " (" + outs.length + " instead of " + channel.parameters.length + ")")

+         else

+           r.locals = ResolveLHS(declaresLocal, outs, channel.parameters, context)

+       case _ => context.Error(r.pos, "receive expression (which has type " + ch.typ.FullName + ") does not denote a channel")

+     }

+ }

 

-  def ResolveLHS(declaresLocal: List[boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = {

-    var locals = List[Variable]()

-    var vars = Set[Variable]()

-    var ctx = context

-    for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) {

-      if (declareLocal) {

-        val local = new Variable(actual.id, new Type(formal.t.typ))

-        locals = locals + local

-        ResolveType(local.t, ctx)

-        actual.Resolve(local)

-        vars = vars + actual.v

-        ctx = ctx.AddVariable(local)

-      } else {

-        ResolveExpr(actual, ctx, false, false)(false)

-        CheckNoGhost(actual, ctx)

-        if (actual.v != null) {

-          if (! canAssign(actual.typ, formal.t.typ))

-            ctx.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " +

-                          formal.t.FullName + ", found: " + actual.typ.FullName + ")")

-          if (vars contains actual.v)

-            ctx.Error(actual.pos, "duplicate actual out-parameter: " + actual.id)

-          else if (actual.v.IsImmutable)

-            ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter")

-          vars = vars + actual.v

-        }

-      }

-    }

-    locals

-  }

+ def ResolveLHS(declaresLocal: List[boolean], actuals: List[VariableExpr], formals: List[Variable], context: ProgramContext): List[Variable] = {

+   var locals = List[Variable]()

+   var vars = Set[Variable]()

+   var ctx = context

+   for (((declareLocal, actual), formal) <- declaresLocal zip actuals zip formals) {

+     if (declareLocal) {

+       val local = new Variable(actual.id, new Type(formal.t.typ))

+       locals = locals + local

+       ResolveType(local.t, ctx)

+       actual.Resolve(local)

+       vars = vars + actual.v

+       ctx = ctx.AddVariable(local)

+     } else {

+       ResolveExpr(actual, ctx, false, false)(false)

+       CheckNoGhost(actual, ctx)

+       if (actual.v != null) {

+         if (! canAssign(actual.typ, formal.t.typ))

+           ctx.Error(actual.pos, "the type of the formal argument is not assignable to the actual parameter (expected: " +

+                         formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+         if (vars contains actual.v)

+           ctx.Error(actual.pos, "duplicate actual out-parameter: " + actual.id)

+         else if (actual.v.IsImmutable)

+           ctx.Error(actual.pos, "cannot use immutable variable " + actual.id + " as actual out-parameter")

+         vars = vars + actual.v

+       }

+     }

+   }

+   locals

+ }

 

-  def ResolveBounds(lowerBounds: List[Expression], upperBounds: List[Expression], context: ProgramContext, descript: String) =

-    for (b <- lowerBounds ++ upperBounds) {

-      ResolveExpr(b, context, true, false)(false)

-      if (!b.typ.IsRef && !b.typ.IsMu)

-        context.Error(b.pos, descript + " bound must be of a reference type or Mu type (found " + b.typ.FullName + ")")

-    }

+ def ResolveBounds(lowerBounds: List[Expression], upperBounds: List[Expression], context: ProgramContext, descript: String) =

+   for (b <- lowerBounds ++ upperBounds) {

+     ResolveExpr(b, context, true, false)(false)

+     if (!b.typ.IsRef && !b.typ.IsMu)

+       context.Error(b.pos, descript + " bound must be of a reference type or Mu type (found " + b.typ.FullName + ")")

+   }

 

-  def ComputeLoopTargets(s: Statement): Set[Variable] = s match {  // local variables

-    case BlockStmt(ss) =>

-      (ss :\ Set[Variable]()) { (s,vars) => vars ++ ComputeLoopTargets(s) }

-    case IfStmt(guard, thn, els) =>

-      val vars = ComputeLoopTargets(thn)

-      els match { case None => vars; case Some(els) => vars ++ ComputeLoopTargets(els) }

-    case w: WhileStmt =>

-      // assume w.LoopTargets is non-null and that it was computed with a larger context

-      w.LoopTargets

-    case Assign(lhs, rhs) =>

-      if (lhs.v != null) Set(lhs.v) else Set()  // don't assume resolution was successful

-    case lv: LocalVar =>

-      lv.rhs match { case None => Set() case Some(_) => Set(lv.v) }

-    case Call(_, lhs, obj, id, args) =>

-      (lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars }

-    case _ => Set()

-  }

+ def ComputeLoopTargets(s: Statement): Set[Variable] = s match {  // local variables

+   case BlockStmt(ss) =>

+     (ss :\ Set[Variable]()) { (s,vars) => vars ++ ComputeLoopTargets(s) }

+   case IfStmt(guard, thn, els) =>

+     val vars = ComputeLoopTargets(thn)

+     els match { case None => vars; case Some(els) => vars ++ ComputeLoopTargets(els) }

+   case w: WhileStmt =>

+     // assume w.LoopTargets is non-null and that it was computed with a larger context

+     w.LoopTargets

+   case Assign(lhs, rhs) =>

+     if (lhs.v != null) Set(lhs.v) else Set()  // don't assume resolution was successful

+   case lv: LocalVar =>

+     lv.rhs match { case None => Set() case Some(_) => Set(lv.v) }

+   case Call(_, lhs, obj, id, args) =>

+     (lhs :\ Set[Variable]()) { (ve,vars) => if (ve.v != null) vars + ve.v else vars }

+   case _ => Set()

+ }

 

-  def ResolveAssign(lhs: VariableExpr, rhs: RValue, context: ProgramContext) = {

-    rhs match {

-      case ExplicitSeq(Nil) => rhs.typ = lhs.typ; // if [] appears on the rhs of an assignment, we "infer" its type by looking at the type of the lhs

-      case _ => ResolveExpr(rhs, context, false, false)(false)

-    }

-    if (! canAssign(lhs.typ, rhs.typ))

-      context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)

-    if (lhs.v != null && !lhs.v.IsGhost) CheckNoGhost(rhs, context)

-  }

+ def ResolveAssign(lhs: VariableExpr, rhs: RValue, context: ProgramContext) = {

+   rhs match {

+     case ExplicitSeq(Nil) => rhs.typ = lhs.typ; // if [] appears on the rhs of an assignment, we "infer" its type by looking at the type of the lhs

+     case _ => ResolveExpr(rhs, context, false, false)(false)

+   }

+   if (! canAssign(lhs.typ, rhs.typ))

+     context.Error(lhs.pos, "type mismatch in assignment, lhs=" + lhs.typ.FullName + " rhs=" + rhs.typ.FullName)

+   if (lhs.v != null && !lhs.v.IsGhost) CheckNoGhost(rhs, context)

+ }

 

-  // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field

-  def ResolveExpr(e: RValue, context: ProgramContext,

-                  twoStateContext: boolean, specContext: boolean)(implicit inPredicate: Boolean): unit = e match {

-    case e @ NewRhs(id, initialization, lower, upper) =>

-      if (context.Decls contains id) {

-        context.Decls(id) match {

-          case ch: Channel =>

-            e.typ = ChannelClass(ch)

-          case cl: Class =>

-            e.typ = cl

-            if (lower != Nil || upper != Nil)

-              context.Error(e.pos, "A new object of a class type is not allowed to have a wait-order bounds clause (use the share statement instead)")

-        }

-        // initialize the fields

-        var fieldNames = Set[String]()

-        for(ini@Init(f, init) <- initialization) {

-          if (fieldNames contains f) {

-            context.Error(ini.pos, "The field " + f + " occurs more than once in initializer.")

-          } else {

-            fieldNames = fieldNames + f

-            e.typ.LookupMember(f) match {

-              case Some(field@Field(name, tp)) =>

-                if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + ".");

-                ResolveExpr(init, context, false, false);

-                if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + ".");

-                ini.f = field;

-              case _ => 

-                context.Error(e.pos, "The type " + id + " does not declare a field " + f + ".");  

-            }

-          }

-        }

-        // resolve the bounds

-        ResolveBounds(lower, upper, context, "new")

-      } else {

-        context.Error(e.pos, "undefined class or channel " + id + " used in new expression")

-        e.typ = IntClass

-      }

-    case i:IntLiteral =>

-      i.typ = IntClass

-    case b:BoolLiteral =>

-      b.typ = BoolClass

-    case n:NullLiteral =>

-      n.typ = NullClass

-    case mx:MaxLockLiteral =>

-      mx.typ = MuClass

-    case mx:LockBottomLiteral =>

-      mx.typ = MuClass

-    case r:Result =>

-      assert(context.CurrentMember!=null);

-      r.typ = IntClass

-      if(context.CurrentMember==null || ! context.CurrentMember.isInstanceOf[Function]){

-        context.Error(r.pos, "The variable result can only be used in the postcondition of a function.");

-      } else {

-        r.typ = context.CurrentMember.asInstanceOf[Function].out.typ;

-      }

-    case ve @ VariableExpr(id) =>

-      context.LookupVariable(id) match {

-        case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass

-        case Some(v) => ve.Resolve(v) }

-    case v:ThisExpr => v.typ = context.CurrentClass

-    case sel @ MemberAccess(e, id) =>

-      ResolveExpr(e, context, twoStateContext, false)

-      var typ: Class = IntClass

-      e.typ.LookupMember(id) match {

-        case None =>

-          context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName)

-        case Some(f: Field) => sel.f = f; typ = f.typ.typ

-        case Some(pred@Predicate(id, body)) =>

-          if(! specContext)

-            context.Error(sel.pos, "predicate can only be used in positive predicate contexts")

-          sel.predicate = pred;

-          sel.isPredicate = true;

-          typ = BoolClass

-        case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);

-      }

-      sel.typ = typ

-    case expr@ Access(e, perm) =>

-      if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")

-      ResolveExpr(e, context, twoStateContext, true)

-      perm match {

-        case None =>

-        case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }

-      expr.typ = BoolClass

-    case expr@ RdAccess(e,perm) =>

-      if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")

-      ResolveExpr(e, context, twoStateContext, true)

-      perm match {

-        case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)

-        case _ => }

-      expr.typ = BoolClass

-    case expr@AccessAll(obj, perm) =>

-      if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")

-      ResolveExpr(obj, context, twoStateContext, false)

-      if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")

-      perm match {

-        case None =>

-        case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }

-      expr.typ = BoolClass

-    case expr@RdAccessAll(obj,perm) =>

-      if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")

-      ResolveExpr(obj, context, twoStateContext, false)

-      if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")

-      perm match {

-        case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)

-        case _ => }

-      expr.typ = BoolClass

-    case expr@ Credit(e,n) =>

-      if (!specContext) context.Error(expr.pos, "credit expression is allowed only in positive predicate contexts")

-      ResolveExpr(e, context, twoStateContext, false)

-      if(!e.typ.IsChannel) context.Error(expr.pos, "credit argument must denote a channel.")

-      ResolveExpr(expr.N, context, twoStateContext, false)

-      expr.typ = BoolClass

-    case expr@ Holds(e) =>

-      if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates")

-      if(! specContext)

-        context.Error(expr.pos, "holds is allowed only in positive predicate contexts"); 

-      //todo: check that we are not in an invariant

-      ResolveExpr(e, context, twoStateContext, false)

-      expr.typ = BoolClass

-    case expr@ RdHolds(e) =>

-      if(inPredicate) context.Error(expr.pos, "rdholds cannot be mentioned in monitor invariants or predicates")

-      ResolveExpr(e, context, twoStateContext, false)

-      expr.typ = BoolClass

-    case expr@ Assigned(id) =>

-      context.LookupVariable(id) match {

-        case None => context.Error(expr.pos, "undefined local variable " + id)

-        case Some(v) =>

-          expr.v = v

-          if (!(v.IsImmutable && v.IsGhost))

-            context.Error(expr.pos, "assigned can only be used with ghost consts")

-      }

-      expr.typ = BoolClass

-    case expr@ Old(e) =>

-      if (! twoStateContext) { context.Error(expr.pos, "old expression is not allowed here") }

-      ResolveExpr(e, context, twoStateContext, false)

-      expr.typ = e.typ

-    case ite@IfThenElse(con, then, els) => 

-      ResolveExpr(con, context, twoStateContext, false); ResolveExpr(then, context, twoStateContext, specContext); ResolveExpr(els, context, twoStateContext, specContext);

-      if (!con.typ.IsBool) context.Error(con.pos, "condition of if-then-else expression must be a boolean");

-      if (! canAssign(then.typ, els.typ)) context.Error(ite.pos, "the then and else branch of an if-then-else expression must have compatible types");

-      ite.typ = then.typ;

-    case expr@ Not(e) =>

-      ResolveExpr(e, context, twoStateContext, false)

-      if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand")

-      expr.typ = BoolClass

-    case appl@FunctionApplication(obj, id, args) =>

-      ResolveExpr(obj, context, twoStateContext, false);

-      args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)};

-      // lookup function

-      appl.typ = IntClass

-      obj.typ.LookupMember(id) match {

-        case None =>

-          context.Error(appl.pos, "function " + id + " not found in class " + obj.typ.FullName)

-        case Some(func@Function(f, ins, out, specs, body)) =>

-          appl.f = func

-          appl.typ = func.out.typ;

-          if (args.length != ins.length)

-            context.Error(appl.pos, "wrong number of actual arguments in function application of " + obj.typ.FullName + "." + id +

-                          " (" + args.length + " instead of " + ins.length + ")")

-          else {

-            for((actual, formal) <- args zip func.ins){

-              if(! canAssign(formal.t.typ, actual.typ))

-                context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

-            }

-          }

-        case _ => context.Error(appl.pos, obj.typ.id + "." + id + " is not a function")

-      }

-    case uf@Unfolding(pred, e) =>

-      ResolveExpr(pred, context, twoStateContext, true);

-      ResolveExpr(e, context, twoStateContext, false);

-      if(! pred.getMemberAccess.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")

-      uf.typ = e.typ;

-    case bin: EqualityCompareExpr =>

-      ResolveExpr(bin.E0, context, twoStateContext, false)

-      ResolveExpr(bin.E1, context, twoStateContext, false)

-      if (bin.E0.typ == bin.E1.typ) { /* all is well */ }

-      else if (bin.E0.typ.IsRef && bin.E1.typ.IsNull) { /* all is well */ }

-      else if (bin.E0.typ.IsNull && bin.E1.typ.IsRef) { /* all is well */ }

-      else

-        context.Error(bin.pos, bin.OpName + " requires operands of the same type, found " + bin.E0.typ.FullName + " and " + bin.E1.typ.FullName)

-      bin.typ = BoolClass

-    case bin: LockBelow =>

-      ResolveExpr(bin.E0, context, twoStateContext, false)

-      ResolveExpr(bin.E1, context, twoStateContext, false)

-      if (!(bin.E0.typ.IsRef || bin.E0.typ.IsMu))

-        context.Error(bin.pos, "type of " + bin.OpName + " LHS operand must be a reference or Mu type (found " + bin.E0.typ.FullName + ")")

-      if (!(bin.E1.typ.IsRef || bin.E1.typ.IsMu))

-        context.Error(bin.pos, "type of " + bin.OpName + " RHS operand must be a reference or Mu type (found " + bin.E1.typ.FullName + ")")

-      bin.typ = BoolClass

-    case app@Append(e0, e1) =>

-      ResolveExpr(e0, context, twoStateContext, false);

-      ResolveExpr(e1, context, twoStateContext, false);

-      if(! e0.typ.IsSeq) context.Error(app.pos, "LHS operand of ++ must be sequence (found: " + e0.typ.FullName + ").");

-      if(! e1.typ.IsSeq) context.Error(app.pos, "RHS operand of ++ must be sequence (found: " + e1.typ.FullName + ").");

-      if(e0.typ != e1.typ) context.Error(app.pos, "++ can only be applied to sequences of the same type.");

-      app.typ = e0.typ;

-    case at@At(e0, e1) =>

-      ResolveExpr(e0, context, twoStateContext, false);

-      ResolveExpr(e1, context, twoStateContext, false);

-      if(! e0.typ.IsSeq) context.Error(at.pos, "LHS operand of @ must be sequence. (found: " + e0.typ.FullName + ").");

-      if(! e1.typ.IsInt) context.Error(at.pos, "RHS operand of @ must be an integer (found: " + e1.typ.FullName + ").");

-      if(e0.typ.IsSeq) at.typ = e0.typ.parameters(0) else at.typ = IntClass;

-    case drop@Drop(e0, e1) =>

-      ResolveExpr(e0, context, twoStateContext, false);

-      ResolveExpr(e1, context, twoStateContext, false);

-      if(! e0.typ.IsSeq) context.Error(drop.pos, "LHS operand of drop must be sequence. (found: " + e0.typ.FullName + ").");

-      if(! e1.typ.IsInt) context.Error(drop.pos, "RHS operand of drop must be an integer (found: " + e1.typ.FullName + ").");

-      drop.typ = e0.typ;

-    case take@Take(e0, e1) =>

-      ResolveExpr(e0, context, twoStateContext, false);

-      ResolveExpr(e1, context, twoStateContext, false);

-      if(! e0.typ.IsSeq) context.Error(take.pos, "LHS operand of take must be sequence. (found: " + e0.typ.FullName + ").");

-      if(! e1.typ.IsInt) context.Error(take.pos, "RHS operand of take must be an integer (found: " + e1.typ.FullName + ").");

-      take.typ = e0.typ;

-    case bin: BinaryExpr =>

-      ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And])

-      ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies]))

-      if (bin.E0.typ != bin.ExpectedLhsType)

-        context.Error(bin.E0.pos, "incorrect type of " + bin.OpName + " LHS" +

-                      " (expected " + bin.ExpectedLhsType.FullName + 

-                      ", found " + bin.E0.typ.FullName + ")")

-      if (bin.E1.typ != bin.ExpectedRhsType)

-        context.Error(bin.E1.pos, "incorrect type of " + bin.OpName + " RHS" +

-                      " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")")

-      bin.typ = bin.ResultType

-    case q: Quantification =>

-      q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") }

-      ResolveExpr(q.Seq, context, twoStateContext, false);

-      if(! q.Seq.typ.IsSeq) 

-        context.Error(q.Seq.pos, "A quantification must range over a sequence. (found: " + q.Seq.typ.FullName + ").");

-      else {

-        val elementType = q.Seq.typ.parameters(0);

-        var bodyContext = context;

-        var bvariables = Nil: List[Variable];

-        q.Is foreach { i =>

-          val variable = new Variable(i, new Type(elementType));

-          bodyContext = bodyContext.AddVariable(variable);

-          bvariables = bvariables + variable;

-        }

-        ResolveExpr(q.E, bodyContext, twoStateContext, true);

-        if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " +  q.E.typ.FullName + ").");

-        q.variables = bvariables;

-      }

-      q.typ = BoolClass

-    case seq@EmptySeq(t) =>

-      ResolveType(t, context)

-      seq.typ = getSeqType(t.typ, context);

-    case seq@ExplicitSeq(es) =>

-      es foreach { e => ResolveExpr(e, context, twoStateContext, false) }

-      es match {

-        case Nil => seq.typ = getSeqType(IntClass, context);

-        case h :: t =>

-          t foreach { e => if(! (e.typ == h.typ)) context.Error(e.pos, "The elements of the sequence expression have different types.")};

-          seq.typ = getSeqType(h.typ, context);

-      }

-    case ran@Range(min, max) =>

-      ResolveExpr(min, context, twoStateContext, false);

-      if(! min.typ.IsInt) context.Error(min.pos, "The mininum of a range expression must be an integer (found: " + min.typ.FullName + ").");

-      ResolveExpr(max, context, twoStateContext, false);

-      if(! max.typ.IsInt) context.Error(max.pos, "The maximum of a range expression must be an integer (found: " + max.typ.FullName + ").");

-      ran.typ = getSeqType(IntClass, context);

-    case len@Length(e) =>

-      ResolveExpr(e, context, twoStateContext, false);

-      if(! e.typ.IsSeq) context.Error(len.pos, "The operand of a length expression must be sequence. (found: " + e.typ.FullName + ").");

-      len.typ = IntClass;

-    case ev@Eval(h, e) =>

-      if(inPredicate) context.Error(ev.pos, "eval cannot be used in monitor invariants or predicates")

-      h match {

-        case AcquireState(obj) => 

-          ResolveExpr(obj, context, twoStateContext, false)

-          if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");

-        case ReleaseState(obj) => ResolveExpr(obj, context, twoStateContext, false)

-          if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");

-        case c@CallState(token, obj, id, args) =>

-          ResolveExpr(token, context, twoStateContext, false);

-          if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens");

-          ResolveExpr(obj, context, false, false)

-          CheckNoGhost(obj, context)

-          args foreach { a => ResolveExpr(a, context, false, false); CheckNoGhost(a, context) }

-          // lookup method

-          var typ: Class = IntClass

-          obj.typ.LookupMember(id) match {

-            case None =>

-              context.Error(obj.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)

-            case Some(m: Method) =>

-              c.m = m

-              if (args.length != m.ins.length)

-                context.Error(obj.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +

-                          " (" + args.length + " instead of " + m.ins.length + ")")

-              else {

-                for((actual, formal) <- args zip m.ins){

-                  if(! canAssign(formal.t.typ, actual.typ))

-                   context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

-              }

-            }

-          case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)

-      }

-            

-          

-      }

-      ResolveExpr(e, context, false, specContext)

-      ev.typ = e.typ;

-  }

+ // ResolveExpr resolves all parts of an RValue, if possible, and (always) sets the RValue's typ field

+ def ResolveExpr(e: RValue, context: ProgramContext,

+                 twoStateContext: boolean, specContext: boolean)(implicit inPredicate: Boolean): unit = e match {

+   case e @ NewRhs(id, initialization, lower, upper) =>

+     if (context.Decls contains id) {

+       context.Decls(id) match {

+         case ch: Channel =>

+           e.typ = ChannelClass(ch)

+         case cl: Class =>

+           e.typ = cl

+           if (lower != Nil || upper != Nil)

+             context.Error(e.pos, "A new object of a class type is not allowed to have a wait-order bounds clause (use the share statement instead)")

+       }

+       // initialize the fields

+       var fieldNames = Set[String]()

+       for(ini@Init(f, init) <- initialization) {

+         if (fieldNames contains f) {

+           context.Error(ini.pos, "The field " + f + " occurs more than once in initializer.")

+         } else {

+           fieldNames = fieldNames + f

+           e.typ.LookupMember(f) match {

+             case Some(field@Field(name, tp)) =>

+               if(field.isInstanceOf[SpecialField]) context.Error(init.pos, "Initializer cannot assign to special field " + name + ".");

+               ResolveExpr(init, context, false, false);

+               if(! canAssign(tp.typ, init.typ)) context.Error(init.pos, "The field " + name + " cannot be initialized with an expression of type " + init.typ.id + ".");

+               ini.f = field;

+             case _ => 

+               context.Error(e.pos, "The type " + id + " does not declare a field " + f + ".");  

+           }

+         }

+       }

+       // resolve the bounds

+       ResolveBounds(lower, upper, context, "new")

+     } else {

+       context.Error(e.pos, "undefined class or channel " + id + " used in new expression")

+       e.typ = IntClass

+     }

+   case i:IntLiteral =>

+     i.typ = IntClass

+   case b:BoolLiteral =>

+     b.typ = BoolClass

+   case n:NullLiteral =>

+     n.typ = NullClass

+   case mx:MaxLockLiteral =>

+     mx.typ = MuClass

+   case mx:LockBottomLiteral =>

+     mx.typ = MuClass

+   case r:Result =>

+     assert(context.CurrentMember!=null);

+     r.typ = IntClass

+     if(context.CurrentMember==null || ! context.CurrentMember.isInstanceOf[Function]){

+       context.Error(r.pos, "The variable result can only be used in the postcondition of a function.");

+     } else {

+       r.typ = context.CurrentMember.asInstanceOf[Function].out.typ;

+     }

+   case ve @ VariableExpr(id) =>

+     context.LookupVariable(id) match {

+       case None => context.Error(ve.pos, "undefined local variable " + id); ve.typ = IntClass

+       case Some(v) => ve.Resolve(v) }

+   case v:ThisExpr => v.typ = context.CurrentClass

+   case sel @ MemberAccess(e, id) =>

+     ResolveExpr(e, context, twoStateContext, false)

+     var typ: Class = IntClass

+     e.typ.LookupMember(id) match {

+       case None =>

+         context.Error(sel.pos, "undeclared member " + id + " in class " + e.typ.FullName)

+       case Some(f: Field) => sel.f = f; typ = f.typ.typ

+       case Some(pred@Predicate(id, body)) =>

+         if(! specContext)

+           context.Error(sel.pos, "predicate can only be used in positive predicate contexts")

+         sel.predicate = pred;

+         sel.isPredicate = true;

+         typ = BoolClass

+       case _ => context.Error(sel.pos, "field-select expression does not denote a field: " + e.typ.FullName + "." + id);

+     }

+     sel.typ = typ

+   case expr@ Access(e, perm) =>

+     if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")

+     ResolveExpr(e, context, twoStateContext, true)

+     perm match {

+       case None =>

+       case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }

+     expr.typ = BoolClass

+   case expr@ RdAccess(e,perm) =>

+     if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")

+     ResolveExpr(e, context, twoStateContext, true)

+     perm match {

+       case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)

+       case _ => }

+     expr.typ = BoolClass

+   case expr@AccessAll(obj, perm) =>

+     if (!specContext) context.Error(expr.pos, "acc expression is allowed only in positive predicate contexts")

+     ResolveExpr(obj, context, twoStateContext, false)

+     if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")

+     perm match {

+       case None =>

+       case Some(perm) => ResolveExpr(perm, context, twoStateContext, false) }

+     expr.typ = BoolClass

+   case expr@RdAccessAll(obj,perm) =>

+     if (!specContext) context.Error(expr.pos, "rd expression is allowed only in positive predicate contexts")

+     ResolveExpr(obj, context, twoStateContext, false)

+     if(!obj.typ.IsRef) context.Error(expr.pos, "Target of .* must be object reference.")

+     perm match {

+       case Some(Some(p)) => ResolveExpr(p, context, twoStateContext, false)

+       case _ => }

+     expr.typ = BoolClass

+   case expr@ Credit(e,n) =>

+     if (!specContext) context.Error(expr.pos, "credit expression is allowed only in positive predicate contexts")

+     ResolveExpr(e, context, twoStateContext, false)

+     if(!e.typ.IsChannel) context.Error(expr.pos, "credit argument must denote a channel.")

+     ResolveExpr(expr.N, context, twoStateContext, false)

+     expr.typ = BoolClass

+   case expr@ Holds(e) =>

+     if(inPredicate) context.Error(expr.pos, "holds cannot be mentioned in monitor invariants or predicates")

+     if(! specContext)

+       context.Error(expr.pos, "holds is allowed only in positive predicate contexts"); 

+     //todo: check that we are not in an invariant

+     ResolveExpr(e, context, twoStateContext, false)

+     expr.typ = BoolClass

+   case expr@ RdHolds(e) =>

+     if(inPredicate) context.Error(expr.pos, "rdholds cannot be mentioned in monitor invariants or predicates")

+     ResolveExpr(e, context, twoStateContext, false)

+     expr.typ = BoolClass

+   case expr@ Assigned(id) =>

+     context.LookupVariable(id) match {

+       case None => context.Error(expr.pos, "undefined local variable " + id)

+       case Some(v) =>

+         expr.v = v

+         if (!(v.IsImmutable && v.IsGhost))

+           context.Error(expr.pos, "assigned can only be used with ghost consts")

+     }

+     expr.typ = BoolClass

+   case expr@ Old(e) =>

+     if (! twoStateContext) { context.Error(expr.pos, "old expression is not allowed here") }

+     ResolveExpr(e, context, twoStateContext, false)

+     expr.typ = e.typ

+   case ite@IfThenElse(con, then, els) => 

+     ResolveExpr(con, context, twoStateContext, false); ResolveExpr(then, context, twoStateContext, specContext); ResolveExpr(els, context, twoStateContext, specContext);

+     if (!con.typ.IsBool) context.Error(con.pos, "condition of if-then-else expression must be a boolean");

+     if (! canAssign(then.typ, els.typ)) context.Error(ite.pos, "the then and else branch of an if-then-else expression must have compatible types");

+     ite.typ = then.typ;

+   case expr@ Not(e) =>

+     ResolveExpr(e, context, twoStateContext, false)

+     if (!e.typ.IsBool) context.Error(expr.pos, "not-expression requires boolean operand")

+     expr.typ = BoolClass

+   case appl@FunctionApplication(obj, id, args) =>

+     ResolveExpr(obj, context, twoStateContext, false);

+     args foreach { arg => ResolveExpr(arg, context, twoStateContext, false)};

+     // lookup function

+     appl.typ = IntClass

+     obj.typ.LookupMember(id) match {

+       case None =>

+         context.Error(appl.pos, "function " + id + " not found in class " + obj.typ.FullName)

+       case Some(func@Function(f, ins, out, specs, body)) =>

+         appl.f = func

+         appl.typ = func.out.typ;

+         if (args.length != ins.length)

+           context.Error(appl.pos, "wrong number of actual arguments in function application of " + obj.typ.FullName + "." + id +

+                         " (" + args.length + " instead of " + ins.length + ")")

+         else {

+           for((actual, formal) <- args zip func.ins){

+             if(! canAssign(formal.t.typ, actual.typ))

+               context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+           }

+         }

+       case _ => context.Error(appl.pos, obj.typ.id + "." + id + " is not a function")

+     }

+   case uf@Unfolding(pred, e) =>

+     ResolveExpr(pred, context, twoStateContext, true);

+     ResolveExpr(e, context, twoStateContext, false);

+     if(! pred.getMemberAccess.isPredicate) context.Error(uf.pos, "Only predicates can be unfolded.")

+     uf.typ = e.typ;

+   case bin: EqualityCompareExpr =>

+     ResolveExpr(bin.E0, context, twoStateContext, false)

+     ResolveExpr(bin.E1, context, twoStateContext, false)

+     if (bin.E0.typ == bin.E1.typ) { /* all is well */ }

+     else if (bin.E0.typ.IsRef && bin.E1.typ.IsNull) { /* all is well */ }

+     else if (bin.E0.typ.IsNull && bin.E1.typ.IsRef) { /* all is well */ }

+     else

+       context.Error(bin.pos, bin.OpName + " requires operands of the same type, found " + bin.E0.typ.FullName + " and " + bin.E1.typ.FullName)

+     bin.typ = BoolClass

+   case bin: LockBelow =>

+     ResolveExpr(bin.E0, context, twoStateContext, false)

+     ResolveExpr(bin.E1, context, twoStateContext, false)

+     if (!(bin.E0.typ.IsRef || bin.E0.typ.IsMu))

+       context.Error(bin.pos, "type of " + bin.OpName + " LHS operand must be a reference or Mu type (found " + bin.E0.typ.FullName + ")")

+     if (!(bin.E1.typ.IsRef || bin.E1.typ.IsMu))

+       context.Error(bin.pos, "type of " + bin.OpName + " RHS operand must be a reference or Mu type (found " + bin.E1.typ.FullName + ")")

+     bin.typ = BoolClass

+   case app@Append(e0, e1) =>

+     ResolveExpr(e0, context, twoStateContext, false);

+     ResolveExpr(e1, context, twoStateContext, false);

+     if(! e0.typ.IsSeq) context.Error(app.pos, "LHS operand of ++ must be sequence (found: " + e0.typ.FullName + ").");

+     if(! e1.typ.IsSeq) context.Error(app.pos, "RHS operand of ++ must be sequence (found: " + e1.typ.FullName + ").");

+     if(e0.typ != e1.typ) context.Error(app.pos, "++ can only be applied to sequences of the same type.");

+     app.typ = e0.typ;

+   case at@At(e0, e1) =>

+     ResolveExpr(e0, context, twoStateContext, false);

+     ResolveExpr(e1, context, twoStateContext, false);

+     if(! e0.typ.IsSeq) context.Error(at.pos, "LHS operand of @ must be sequence. (found: " + e0.typ.FullName + ").");

+     if(! e1.typ.IsInt) context.Error(at.pos, "RHS operand of @ must be an integer (found: " + e1.typ.FullName + ").");

+     if(e0.typ.IsSeq) at.typ = e0.typ.parameters(0) else at.typ = IntClass;

+   case drop@Drop(e0, e1) =>

+     ResolveExpr(e0, context, twoStateContext, false);

+     ResolveExpr(e1, context, twoStateContext, false);

+     if(! e0.typ.IsSeq) context.Error(drop.pos, "LHS operand of drop must be sequence. (found: " + e0.typ.FullName + ").");

+     if(! e1.typ.IsInt) context.Error(drop.pos, "RHS operand of drop must be an integer (found: " + e1.typ.FullName + ").");

+     drop.typ = e0.typ;

+   case take@Take(e0, e1) =>

+     ResolveExpr(e0, context, twoStateContext, false);

+     ResolveExpr(e1, context, twoStateContext, false);

+     if(! e0.typ.IsSeq) context.Error(take.pos, "LHS operand of take must be sequence. (found: " + e0.typ.FullName + ").");

+     if(! e1.typ.IsInt) context.Error(take.pos, "RHS operand of take must be an integer (found: " + e1.typ.FullName + ").");

+     take.typ = e0.typ;

+   case bin: BinaryExpr =>

+     ResolveExpr(bin.E0, context, twoStateContext, specContext && bin.isInstanceOf[And])

+     ResolveExpr(bin.E1, context, twoStateContext, specContext && (bin.isInstanceOf[And] || bin.isInstanceOf[Implies]))

+     if (bin.E0.typ != bin.ExpectedLhsType)

+       context.Error(bin.E0.pos, "incorrect type of " + bin.OpName + " LHS" +

+                     " (expected " + bin.ExpectedLhsType.FullName + 

+                     ", found " + bin.E0.typ.FullName + ")")

+     if (bin.E1.typ != bin.ExpectedRhsType)

+       context.Error(bin.E1.pos, "incorrect type of " + bin.OpName + " RHS" +

+                     " (expected " + bin.ExpectedRhsType.FullName + ", found " + bin.E1.typ.FullName + ")")

+     bin.typ = bin.ResultType

+   case q: Quantification =>

+     q.Is foreach { i => if(context.LookupVariable(i).isDefined) context.Error(q.pos, "The variable " + i + " hides another local.") }

+     ResolveExpr(q.Seq, context, twoStateContext, false);

+     if(! q.Seq.typ.IsSeq) 

+       context.Error(q.Seq.pos, "A quantification must range over a sequence. (found: " + q.Seq.typ.FullName + ").");

+     else {

+       val elementType = q.Seq.typ.parameters(0);

+       var bodyContext = context;

+       var bvariables = Nil: List[Variable];

+       q.Is foreach { i =>

+         val variable = new Variable(i, new Type(elementType));

+         bodyContext = bodyContext.AddVariable(variable);

+         bvariables = bvariables + variable;

+       }

+       ResolveExpr(q.E, bodyContext, twoStateContext, true);

+       if(! q.E.typ.IsBool) context.Error(q.E.pos, "Body of quantification must be a boolean. (found: " +  q.E.typ.FullName + ").");

+       q.variables = bvariables;

+     }

+     q.typ = BoolClass

+   case seq@EmptySeq(t) =>

+     ResolveType(t, context)

+     seq.typ = getSeqType(t.typ, context);

+   case seq@ExplicitSeq(es) =>

+     es foreach { e => ResolveExpr(e, context, twoStateContext, false) }

+     es match {

+       case Nil => seq.typ = getSeqType(IntClass, context);

+       case h :: t =>

+         t foreach { e => if(! (e.typ == h.typ)) context.Error(e.pos, "The elements of the sequence expression have different types.")};

+         seq.typ = getSeqType(h.typ, context);

+     }

+   case ran@Range(min, max) =>

+     ResolveExpr(min, context, twoStateContext, false);

+     if(! min.typ.IsInt) context.Error(min.pos, "The mininum of a range expression must be an integer (found: " + min.typ.FullName + ").");

+     ResolveExpr(max, context, twoStateContext, false);

+     if(! max.typ.IsInt) context.Error(max.pos, "The maximum of a range expression must be an integer (found: " + max.typ.FullName + ").");

+     ran.typ = getSeqType(IntClass, context);

+   case len@Length(e) =>

+     ResolveExpr(e, context, twoStateContext, false);

+     if(! e.typ.IsSeq) context.Error(len.pos, "The operand of a length expression must be sequence. (found: " + e.typ.FullName + ").");

+     len.typ = IntClass;

+   case ev@Eval(h, e) =>

+     if(inPredicate) context.Error(ev.pos, "eval cannot be used in monitor invariants or predicates")

+     h match {

+       case AcquireState(obj) => 

+         ResolveExpr(obj, context, twoStateContext, false)

+         if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");

+       case ReleaseState(obj) => ResolveExpr(obj, context, twoStateContext, false)

+         if(! obj.typ.IsRef) context.Error(ev.pos, "The target of acquire must be a reference.");

+       case c@CallState(token, obj, id, args) =>

+         ResolveExpr(token, context, twoStateContext, false);

+         if( ! token.typ.IsToken) context.Error(token.pos, "joinable is only applicable to tokens");

+         ResolveExpr(obj, context, false, false)

+         CheckNoGhost(obj, context)

+         args foreach { a => ResolveExpr(a, context, false, false); CheckNoGhost(a, context) }

+         // lookup method

+         var typ: Class = IntClass

+         obj.typ.LookupMember(id) match {

+           case None =>

+             context.Error(obj.pos, "call of undeclared member " + id + " in class " + obj.typ.FullName)

+           case Some(m: Method) =>

+             c.m = m

+             if (args.length != m.ins.length)

+               context.Error(obj.pos, "wrong number of actual in-parameters in call to " + obj.typ.FullName + "." + id +

+                         " (" + args.length + " instead of " + m.ins.length + ")")

+             else {

+               for((actual, formal) <- args zip m.ins){

+                 if(! canAssign(formal.t.typ, actual.typ))

+                  context.Error(actual.pos, "the type of the actual argument is not assignable to the formal parameter (expected: " + formal.t.FullName + ", found: " + actual.typ.FullName + ")")

+             }

+           }

+         case _ => context.Error(obj.pos, "call expression does not denote a method: " + obj.typ.FullName + "." + id)

+     }

+           

+         

+     }

+     ResolveExpr(e, context, false, specContext)

+     ev.typ = e.typ;

+ }

 

-  def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = {

-    cl.LookupMember("run") match {

-      case None =>

-        context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +

-                      " (found type " + cl.id + ")")

-        None

-      case Some(m: Method) =>

-        m.spec foreach {

-          case Precondition(e) => CheckRunSpecification(e, context, true)

-          case Postcondition(e) => CheckRunSpecification(e, context, false)

-          case lc: LockChange => context.Error(lc.pos, "lockchange is not allowed in specification of run method")

-        }

-        if(0<m.ins.length || 0<m.outs.length) {

-          context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +

-                      " (found " + m.ins.length + " in-parameters and " + m.outs.length + " out-parameters)"); None

-        } else

-          Some(m)

-      case _ =>

-        context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +

-                      " (found non-method member)")

-        None

-    }

-  }

+ def LookupRunMethod(cl: Class, context: ProgramContext, op: String, pos: Position): Option[Method] = {

+   cl.LookupMember("run") match {

+     case None =>

+       context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +

+                     " (found type " + cl.id + ")")

+       None

+     case Some(m: Method) =>

+       m.spec foreach {

+         case Precondition(e) => CheckRunSpecification(e, context, true)

+         case Postcondition(e) => CheckRunSpecification(e, context, false)

+         case lc: LockChange => context.Error(lc.pos, "lockchange is not allowed in specification of run method")

+       }

+       if(0<m.ins.length || 0<m.outs.length) {

+         context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +

+                     " (found " + m.ins.length + " in-parameters and " + m.outs.length + " out-parameters)"); None

+       } else

+         Some(m)

+     case _ =>

+       context.Error(pos, "object given in " + op + " statement must be of a type with a parameter-less run method" +

+                     " (found non-method member)")

+       None

+   }

+ }

 

-  // assumes that lhs and rhs are resolved

-  def canAssign(lhs: Class, rhs: Class): Boolean = {

-    (lhs, rhs) match {

-      case (TokenClass(c1, m1), TokenClass(c2, m2)) => c1.id.equals(c2.id) && m1.equals(m2)

-      case (TokenClass(c1, m1), _) => false

-      case (_, TokenClass(c2, m2)) => false

-      case (lhs, rhs) => lhs == rhs || (lhs.IsRef && rhs.IsNull)

-    }

-  }

+ // assumes that lhs and rhs are resolved

+ def canAssign(lhs: Class, rhs: Class): Boolean = {

+   (lhs, rhs) match {

+     case (TokenClass(c1, m1), TokenClass(c2, m2)) => c1.id.equals(c2.id) && m1.equals(m2)

+     case (TokenClass(c1, m1), _) => false

+     case (_, TokenClass(c2, m2)) => false

+     case (lhs, rhs) => lhs == rhs || (lhs.IsRef && rhs.IsNull)

+   }

+ }

 

-  def CheckNoGhost(expr: RValue, context: ProgramContext): Unit = {

-    def specOk(e: RValue): Unit = { 

-      e match {

-        case ve: VariableExpr =>

-          if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here")

-        case fs@ MemberAccess(e, id) =>

-          if (!fs.isPredicate && fs.f != null && fs.f.IsGhost) context.Error(fs.pos, "ghost fields not allowed here")

-          CheckNoGhost(e, context)

-        case a: Assigned =>

-          if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here")

-        case _ => visitE(e, specOk)

-      }

-    }

-    specOk(expr)

-  }

+ def CheckNoGhost(expr: RValue, context: ProgramContext): Unit = {

+   def specOk(e: RValue): Unit = { 

+     e match {

+       case ve: VariableExpr =>

+         if (ve.v != null && ve.v.IsGhost) context.Error(ve.pos, "ghost variable not allowed here")

+       case fs@ MemberAccess(e, id) =>

+         if (!fs.isPredicate && fs.f != null && fs.f.IsGhost) context.Error(fs.pos, "ghost fields not allowed here")

+         CheckNoGhost(e, context)

+       case a: Assigned =>

+         if (a.v != null && a.v.IsGhost) context.Error(a.pos, "ghost variable not allowed here")

+       case _ => visitE(e, specOk)

+     }

+   }

+   specOk(expr)

+ }

 

-  def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = {

-    def specOk(e: RValue): Unit = { 

-      e match {

-        case ve: VariableExpr =>

-          if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here")

-        case a: Assigned =>

-          if (a.v != null && a.v.IsGhost && a.v.IsImmutable) context.Error(a.pos, "ghost const not allowed here")

-        case _ => visitE(e, specOk)

-      }

-    }

-    specOk(expr)

-  }

+ def CheckNoImmutableGhosts(expr: RValue, context: ProgramContext): Unit = {

+   def specOk(e: RValue): Unit = { 

+     e match {

+       case ve: VariableExpr =>

+         if (ve.v != null && ve.v.IsGhost && ve.v.IsImmutable) context.Error(ve.pos, "ghost const not allowed here")

+       case a: Assigned =>

+         if (a.v != null && a.v.IsGhost && a.v.IsImmutable) context.Error(a.pos, "ghost const not allowed here")

+       case _ => visitE(e, specOk)

+     }

+   }

+   specOk(expr)

+ }

 

-  def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: boolean): unit = e match {

-    case _:MaxLockLiteral =>

-      if (!allowMaxLock) context.Error(e.pos, "specification of run method is not allowed to mention maxlock here")

-    case _:Literal =>

-    case _:VariableExpr =>

-    case _:ThisExpr =>

-    case _:Result =>

-    case MemberAccess(e, id) =>

-      CheckRunSpecification(e, context, false)

-    case Access(e, perm) =>

-      CheckRunSpecification(e, context, false)

-      perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }

-    case RdAccess(e, perm) =>

-      CheckRunSpecification(e, context, false)

-      perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }

-    case AccessAll(obj, perm) =>

-      CheckRunSpecification(obj, context, false)

-      perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }

-    case RdAccessAll(obj, perm) =>

-      CheckRunSpecification(obj, context, false)

-      perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }

-    case expr@ Credit(e, n) =>

-      CheckRunSpecification(e, context, false)

-      CheckRunSpecification(expr.N, context, false)

-    case Holds(e) =>

-      context.Error(e.pos, "holds is not allowed in specification of run method")

-    case RdHolds(e) =>

-      context.Error(e.pos, "rd holds is not allowed in specification of run method")

-    case _:Assigned =>

-    case Old(e) =>

-      CheckRunSpecification(e, context, false)  // OLD occurs only in postconditions and monitor invariants, where maxlock is not allowed anyhow

-    case IfThenElse(con, then, els) =>

-      CheckRunSpecification(con, context, false);

-      CheckRunSpecification(con, context, allowMaxLock); 

-      CheckRunSpecification(con, context, allowMaxLock); 

-    case Not(e) =>

-      CheckRunSpecification(e, context, false)

-    case FunctionApplication(obj, id, args) =>

-      obj :: args foreach { arg => CheckRunSpecification(arg, context, false)} 

-    case Unfolding(pred, e) =>

-      CheckRunSpecification(pred, context, true);

-      CheckRunSpecification(e, context, allowMaxLock);

-    case LockBelow(e0,e1) =>

-      CheckRunSpecification(e0, context, allowMaxLock)

-      CheckRunSpecification(e1, context, false)

-    case And(e0,e1) =>

-      CheckRunSpecification(e0, context, allowMaxLock)

-      CheckRunSpecification(e1, context, allowMaxLock)

-    case Implies(e0,e1) =>

-      CheckRunSpecification(e0, context, false)

-      CheckRunSpecification(e1, context, allowMaxLock)

-    case bin: BinaryExpr =>

-      CheckRunSpecification(bin.E0, context, false)

-      CheckRunSpecification(bin.E1, context, false)

-    case q: Quantification =>

-      CheckRunSpecification(q.Seq, context, false)

-      CheckRunSpecification(q.E, context, true)

-    case Length(e) =>

-      CheckRunSpecification(e, context, false);

-    case ExplicitSeq(es) =>

-      es foreach { e => CheckRunSpecification(e, context, false) }

-    case Range(min, max) =>

-      CheckRunSpecification(min, context, false)

-      CheckRunSpecification(max, context, false)

-    case Eval(h, e) =>

-      h match {

-        case AcquireState(obj) =>  CheckRunSpecification(obj, context, false);

-        case ReleaseState(obj) =>  CheckRunSpecification(obj, context, false);

-        case CallState(token, obj, id, args) => CheckRunSpecification(token, context, false); CheckRunSpecification(obj, context, false);  args foreach { a: Expression => CheckRunSpecification(a, context, false)};

-      }

-      CheckRunSpecification(e, context, allowMaxLock)

-  }

+ def CheckRunSpecification(e: Expression, context: ProgramContext, allowMaxLock: boolean): unit = e match {

+   case _:MaxLockLiteral =>

+     if (!allowMaxLock) context.Error(e.pos, "specification of run method is not allowed to mention waitlevel here")

+   case _:Literal =>

+   case _:VariableExpr =>

+   case _:ThisExpr =>

+   case _:Result =>

+   case MemberAccess(e, id) =>

+     CheckRunSpecification(e, context, false)

+   case Access(e, perm) =>

+     CheckRunSpecification(e, context, false)

+     perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }

+   case RdAccess(e, perm) =>

+     CheckRunSpecification(e, context, false)

+     perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }

+   case AccessAll(obj, perm) =>

+     CheckRunSpecification(obj, context, false)

+     perm match { case None => case Some(perm) => CheckRunSpecification(perm, context, false) }

+   case RdAccessAll(obj, perm) =>

+     CheckRunSpecification(obj, context, false)

+     perm match { case Some(Some(p)) => CheckRunSpecification(p, context, false) case _ => }

+   case expr@ Credit(e, n) =>

+     CheckRunSpecification(e, context, false)

+     CheckRunSpecification(expr.N, context, false)

+   case Holds(e) =>

+     context.Error(e.pos, "holds is not allowed in specification of run method")

+   case RdHolds(e) =>

+     context.Error(e.pos, "rd holds is not allowed in specification of run method")

+   case _:Assigned =>

+   case Old(e) =>

+     CheckRunSpecification(e, context, false)  // OLD occurs only in postconditions and monitor invariants, where waitlevel is not allowed anyhow

+   case IfThenElse(con, then, els) =>

+     CheckRunSpecification(con, context, false);

+     CheckRunSpecification(con, context, allowMaxLock); 

+     CheckRunSpecification(con, context, allowMaxLock); 

+   case Not(e) =>

+     CheckRunSpecification(e, context, false)

+   case FunctionApplication(obj, id, args) =>

+     obj :: args foreach { arg => CheckRunSpecification(arg, context, false)} 

+   case Unfolding(pred, e) =>

+     CheckRunSpecification(pred, context, true);

+     CheckRunSpecification(e, context, allowMaxLock);

+   case LockBelow(e0,e1) =>

+     CheckRunSpecification(e0, context, allowMaxLock)

+     CheckRunSpecification(e1, context, false)

+   case And(e0,e1) =>

+     CheckRunSpecification(e0, context, allowMaxLock)

+     CheckRunSpecification(e1, context, allowMaxLock)

+   case Implies(e0,e1) =>

+     CheckRunSpecification(e0, context, false)

+     CheckRunSpecification(e1, context, allowMaxLock)

+   case bin: BinaryExpr =>

+     CheckRunSpecification(bin.E0, context, false)

+     CheckRunSpecification(bin.E1, context, false)

+   case q: Quantification =>

+     CheckRunSpecification(q.Seq, context, false)

+     CheckRunSpecification(q.E, context, true)

+   case Length(e) =>

+     CheckRunSpecification(e, context, false);

+   case ExplicitSeq(es) =>

+     es foreach { e => CheckRunSpecification(e, context, false) }

+   case Range(min, max) =>

+     CheckRunSpecification(min, context, false)

+     CheckRunSpecification(max, context, false)

+   case Eval(h, e) =>

+     h match {

+       case AcquireState(obj) =>  CheckRunSpecification(obj, context, false);

+       case ReleaseState(obj) =>  CheckRunSpecification(obj, context, false);

+       case CallState(token, obj, id, args) => CheckRunSpecification(token, context, false); CheckRunSpecification(obj, context, false);  args foreach { a: Expression => CheckRunSpecification(a, context, false)};

+     }

+     CheckRunSpecification(e, context, allowMaxLock)

+ }

 

-  def visitE(expr: RValue, func: RValue => Unit): Unit = {

-    expr match {

-      case _:NewRhs =>

-      case e: Literal => ;

-      case _:ThisExpr => ;

-      case _:Result => ;

-      case e:VariableExpr => ;

-      case acc@MemberAccess(e,f) =>

-        func(e);

-      case Access(e, perm) =>

-        func(e); perm match { case Some(p) => func(p); case _ => ; }

-      case RdAccess(e, perm) =>

-        func(e); perm match { case Some(Some(p)) => func(p); case _ => ; }

-      case AccessAll(obj, perm) =>

-        func(obj); perm match { case Some(p) => func(p); case _ => ; }

-      case RdAccessAll(obj, perm) =>

-        func(obj); perm match { case Some(Some(p)) => func(p); case _ => ; }

-      case Credit(e, n) =>

-        func(e); n match { case Some(n) => func(n); case _ => }

-      case Holds(e) => func(e);

-      case RdHolds(e) => func(e);

-      case e: Assigned => e

-      case Old(e) => func(e);

-      case IfThenElse(con, then, els) => func(con); func(then); func(els);

-      case Not(e) => func(e);

-      case funapp@FunctionApplication(obj, id, args) =>

-        func(obj); args foreach { arg => func(arg) };

-      case Unfolding(pred, e) =>

-        func(pred); func(e); 

-      case Iff(e0,e1) => func(e0); func(e1);

-      case Implies(e0,e1) => func(e0); func(e1);

-      case And(e0,e1) =>func(e0); func(e1);

-      case Or(e0,e1) => func(e0); func(e1);

-      case Eq(e0,e1) => func(e0); func(e1);

-      case Neq(e0,e1) => func(e0); func(e1);

-      case Less(e0,e1) => func(e0); func(e1);

-      case AtMost(e0,e1) => func(e0); func(e1);

-      case AtLeast(e0,e1) => func(e0); func(e1);

-      case Greater(e0,e1) => func(e0); func(e1);

-      case LockBelow(e0,e1) => func(e0); func(e1);

-      case Plus(e0,e1) => func(e0); func(e1);

-      case Minus(e0,e1) => func(e0); func(e1);

-      case Times(e0,e1) => func(e0); func(e1);

-      case Div(e0,e1) => func(e0); func(e1);

-      case Mod(e0,e1) => func(e0); func(e1);

-      case Forall(i, seq, e) => func(seq); func(e);

-      case ExplicitSeq(es) =>

-        es foreach { e => func(e) }

-      case Range(min, max) =>

-        func(min); func(max);

-      case Append(e0, e1) =>

-        func(e0); func(e1);

-      case at@At(e0, e1) =>

-        func(e0); func(e1);

-      case Drop(e0, e1) =>

-        func(e0); func(e1);

-      case Take(e0, e1) =>

-        func(e0); func(e1);

-      case Length(e) =>

-        func(e)

-      case Eval(h, e) =>

-        h match {

-          case AcquireState(obj) => func(obj);

-          case ReleaseState(obj) => func(obj);

-          case CallState(token, obj, id, args) => func(token); func(obj); args foreach {a : Expression => func(a)};

-        }

-        func(e);

-    }

-  }

+ def visitE(expr: RValue, func: RValue => Unit): Unit = {

+   expr match {

+     case _:NewRhs =>

+     case e: Literal => ;

+     case _:ThisExpr => ;

+     case _:Result => ;

+     case e:VariableExpr => ;

+     case acc@MemberAccess(e,f) =>

+       func(e);

+     case Access(e, perm) =>

+       func(e); perm match { case Some(p) => func(p); case _ => ; }

+     case RdAccess(e, perm) =>

+       func(e); perm match { case Some(Some(p)) => func(p); case _ => ; }

+     case AccessAll(obj, perm) =>

+       func(obj); perm match { case Some(p) => func(p); case _ => ; }

+     case RdAccessAll(obj, perm) =>

+       func(obj); perm match { case Some(Some(p)) => func(p); case _ => ; }

+     case Credit(e, n) =>

+       func(e); n match { case Some(n) => func(n); case _ => }

+     case Holds(e) => func(e);

+     case RdHolds(e) => func(e);

+     case e: Assigned => e

+     case Old(e) => func(e);

+     case IfThenElse(con, then, els) => func(con); func(then); func(els);

+     case Not(e) => func(e);

+     case funapp@FunctionApplication(obj, id, args) =>

+       func(obj); args foreach { arg => func(arg) };

+     case Unfolding(pred, e) =>

+       func(pred); func(e); 

+     case Iff(e0,e1) => func(e0); func(e1);

+     case Implies(e0,e1) => func(e0); func(e1);

+     case And(e0,e1) =>func(e0); func(e1);

+     case Or(e0,e1) => func(e0); func(e1);

+     case Eq(e0,e1) => func(e0); func(e1);

+     case Neq(e0,e1) => func(e0); func(e1);

+     case Less(e0,e1) => func(e0); func(e1);

+     case AtMost(e0,e1) => func(e0); func(e1);

+     case AtLeast(e0,e1) => func(e0); func(e1);

+     case Greater(e0,e1) => func(e0); func(e1);

+     case LockBelow(e0,e1) => func(e0); func(e1);

+     case Plus(e0,e1) => func(e0); func(e1);

+     case Minus(e0,e1) => func(e0); func(e1);

+     case Times(e0,e1) => func(e0); func(e1);

+     case Div(e0,e1) => func(e0); func(e1);

+     case Mod(e0,e1) => func(e0); func(e1);

+     case Forall(i, seq, e) => func(seq); func(e);

+     case ExplicitSeq(es) =>

+       es foreach { e => func(e) }

+     case Range(min, max) =>

+       func(min); func(max);

+     case Append(e0, e1) =>

+       func(e0); func(e1);

+     case at@At(e0, e1) =>

+       func(e0); func(e1);

+     case Drop(e0, e1) =>

+       func(e0); func(e1);

+     case Take(e0, e1) =>

+       func(e0); func(e1);

+     case Length(e) =>

+       func(e)

+     case Eval(h, e) =>

+       h match {

+         case AcquireState(obj) => func(obj);

+         case ReleaseState(obj) => func(obj);

+         case CallState(token, obj, id, args) => func(token); func(obj); args foreach {a : Expression => func(a)};

+       }

+       func(e);

+   }

+ }

 }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 6b85ed8a..7a85ef74 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -34,7 +34,7 @@ class Translator {
     decls flatMap {

       case cl: Class => translateClass(cl)

       case ch: Channel => translateClass(ChannelClass(ch)) /* TODO: admissibility check of where clause */

-        /* TODO: maxlock not allowed in postcondition of things forked (or, rather, joined) */

+        /* TODO: waitlevel not allowed in postcondition of things forked (or, rather, joined) */

     }

   }

 

@@ -156,7 +156,7 @@ class Translator {
     val version = Version(Preconditions(f.spec).foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }), etran);

     val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)});

     val frameFunctionName = "##" + f.FullName;

-    

+

     /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n ::

          wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body))

     */

@@ -537,7 +537,7 @@ class Translator {
         val formalThis = new VariableExpr(formalThisV)

         val formalInsV = for (p <- c.m.ins) yield new Variable(p.id, p.t)

         val formalIns = for (v <- formalInsV) yield new VariableExpr(v)

-        

+

         val (tokenV,tokenId) = NewBVar("token", tref, true)

         val (asyncStateV,asyncState) = NewBVar("asyncstate", tint, true)

         val (preCallHeapV, preCallHeap) = NewBVar("preCallHeap", theap, true)

@@ -668,9 +668,9 @@ class Translator {
         bassert(nonNull(ch), ch.pos, "The channel might be null.") ::

         // check that credits are positive

         bassert(0 < new Boogie.MapSelect(etran.Credits, TrExpr(ch)), r.pos, "receive operation requires a credit") ::

-        // ...and check: maxlock << ch.mu

+        // ...and check: waitlevel << ch.mu

         bassert(CanRead(ch, "mu"), r.pos, "The mu field of the channel in the receive statement might not be readable.") ::

-        bassert(etran.MaxLockIsBelowX(etran.Heap.select(ch, "mu")), r.pos, "The channel must lie above maxlock in the wait order") ::

+        bassert(etran.MaxLockIsBelowX(etran.Heap.select(ch, "mu")), r.pos, "The channel must lie above waitlevel in the wait order") ::

         // introduce locals for the parameters

         (for (v <- formalThisV :: formalParamsV) yield BLocal(Variable2BVarWhere(v))) :::

         // initialize the parameters; that is, set "this" to the channel and havoc the other formal parameters

@@ -686,7 +686,7 @@ class Translator {
         new Boogie.MapUpdate(etran.Credits, TrExpr(ch), new Boogie.MapSelect(etran.Credits, TrExpr(ch)) - 1)

     }

   }

-  

+

   def translateAllocation(cl: Class, initialization: List[Init], lowerBounds: List[Expression], upperBounds: List[Expression], pos: Position): (Boogie.BVar, List[Boogie.Stmt]) = {

     val (nw, nwe) = NewBVar("nw", Boogie.ClassType(cl), true)

     val (ttV,tt) = Boogie.NewTVar("T")

@@ -721,7 +721,7 @@ class Translator {
        bassume(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")))

      else

        bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the acquire statement might not be readable.") ::

-       bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above maxlock.")) :::

+       bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above waitlevel.")) :::

     bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) ::  // this isn't strictly necessary, it seems; but we might as well include it

     // remember the state right before releasing

     BLocal(lastSeenMuV) :: (lastSeenMu := etran.Heap.select(o, "mu")) ::

@@ -770,7 +770,7 @@ class Translator {
     val (heldV, held) = Boogie.NewBVar("held", tint, true)

     val o = TrExpr(nonNullObj)

     bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the read-acquire statement might not be readable.") ::

-    bassert(etran.MaxLockIsBelowX(etran.Heap.select(o, "mu")), s.pos, "The mu field of the target of the read-acquire statement might not be above maxlock.") ::

+    bassert(etran.MaxLockIsBelowX(etran.Heap.select(o, "mu")), s.pos, "The mu field of the target of the read-acquire statement might not be above waitlevel.") ::

     bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) ::  // this isn't strictly necessary, it seems; but we might as well include it

     bassume(! isHeld(o) && ! isRdHeld(o)) ::

     BLocal(heldV) :: Havoc(held) :: bassume(held <= 0) ::

@@ -857,7 +857,7 @@ class Translator {
     (loopEtran.oldEtran.Credits := loopEtran.Credits) ::  // is oldCredits?

     // check invariant on entry to the loop

     Exhale(invs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant might not hold on entry to the loop."))}, "loop invariant, initially") :::

-	List(bassert(DebtCheck, w.pos, "Loop invariant must consume all debt on entry to the loop.")) :::

+     List(bassert(DebtCheck, w.pos, "Loop invariant must consume all debt on entry to the loop.")) :::

     // save values of local-variable loop targets

     (for (sv <- saveLocalsV) yield BLocal(Variable2BVarWhere(sv))) :::

     (for ((v,sv) <- w.LoopTargetsList zip saveLocalsV) yield

@@ -948,9 +948,9 @@ class Translator {
                   Below(MuValue(lb), MuValue(ub)) }, lb.pos, "The lower bound at " + lb.pos + " might not be smaller than the upper bound at " + ub.pos + ".")) :::

     // havoc mu

     BLocal(muV) :: Havoc(mu) :: bassume(mu !=@ bLockBottom) ::

-    // assume that mu is between the given bounds (or above maxlock if no bounds are given)

+    // assume that mu is between the given bounds (or above waitlevel if no bounds are given)

     (if (lowerBounds == Nil && upperBounds == Nil) {

-      // assume maxlock << mu

+      // assume waitlevel << mu

       List(bassume(etran.MaxLockIsBelowX(mu)))

     } else {

       (for (lb <- lowerBounds) yield

@@ -1129,7 +1129,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   /**********************************************************************

   *****************              TR/DF                  *****************

   **********************************************************************/

- 

+

   def isDefined(e: Expression)(implicit assumption: Expr): List[Boogie.Stmt] = {

     def prove(goal: Expr, pos: Position, msg: String)(implicit assumption: Expr): Boogie.Assert = {

       bassert(assumption ==> goal, pos, msg)

@@ -1302,7 +1302,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     case IntLiteral(n) => n

     case BoolLiteral(b) => b

     case NullLiteral() => bnull

-    case MaxLockLiteral() => throw new Exception("maxlock case should be handled in << and == and !=")

+    case MaxLockLiteral() => throw new Exception("waitlevel case should be handled in << and == and !=")

     case LockBottomLiteral() => bLockBottom

     case _:ThisExpr => VarExpr("this")

     case _:Result => VarExpr("result")

@@ -1425,7 +1425,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       val evalEtran = new ExpressionTranslator(List(evalHeap, evalMask, evalCredits), currentClass);

       evalEtran.Tr(e)

   }

- 

+

   def translateForall(is: List[Variable], min: Expression, max: Expression, e: Expression): Expr = {

     var assumption = true: Expr;

     for(i <- is) {

@@ -1745,7 +1745,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
          isDefined(obj)(true), true)

       case CallState(token, obj, id, args) =>

         val argsSeq = CallArgs(Heap.select(Tr(token), "joinable"));

-        

+

         var i : int = 0;

         (CallHeap(Heap.select(Tr(token), "joinable")), 

          CallMask(Heap.select(Tr(token), "joinable")),

@@ -1760,7 +1760,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
         )

     }

   }

- 

+

   // permissions

 

   def CanRead(obj: Boogie.Expr, field: Boogie.Expr): Boogie.Expr = new Boogie.FunctionApp("CanRead", Mask, obj, field)

@@ -1829,14 +1829,14 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   def IncPerm(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncPerm", List(m, e, f, i))

   def IncEpsilons(m: Expr, e: Expr, f: Expr, i: Expr) = FunctionApp("IncEpsilons", List(m, e, f, i))

 

-  

-  def MaxLockIsBelowX(x: Boogie.Expr) = {  // maxlock << x

+

+  def MaxLockIsBelowX(x: Boogie.Expr) = {  // waitlevel << x

     val (oV, o) = Boogie.NewBVar("o", tref, false)

     new Boogie.Forall(oV,

                       (contributesToWaitLevel(o, Heap, Credits)) ==>

                       new Boogie.FunctionApp("MuBelow", Boogie.MapSelect(Heap, o, "mu"), x))

   }

-  def MaxLockIsAboveX(x: Boogie.Expr) = {  // x << maxlock

+  def MaxLockIsAboveX(x: Boogie.Expr) = {  // x << waitlevel

     val (oV, o) = Boogie.NewBVar("o", tref, false)

     new Boogie.Exists(oV,

                       (contributesToWaitLevel(o, Heap, Credits)) &&

@@ -1850,7 +1850,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
                         (new Boogie.FunctionApp("MuBelow", MapSelect(Heap, r, "mu"), x) ||

                         (Boogie.MapSelect(Heap, r, "mu") ==@ x)))

   }

-  def MaxLockPreserved = {  // old(maxlock) == maxlock

+  def MaxLockPreserved = {  // old(waitlevel) == waitlevel

     // I don't know what the best encoding of this conding is, so I'll try a disjunction.

     // Disjunct b0 is easier to prove, but it is stronger than b1.

 

@@ -1881,7 +1881,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
                   (Boogie.MapSelect(oldEtran.Heap, o, "mu") ==@ Boogie.MapSelect(Heap, p, "mu")))

     b0 || b1

   }

-  def TemporalMaxLockComparison(e0: ExpressionTranslator, e1: ExpressionTranslator) = {  // e0(maxlock) << e1(maxlock)

+  def TemporalMaxLockComparison(e0: ExpressionTranslator, e1: ExpressionTranslator) = {  // e0(waitlevel) << e1(waitlevel)

     // (exists o ::

     //     e1(o.held) &&

     //     (forall r :: e0(r.held) ==> e0(r.mu) << e1(o.mu)))

@@ -2063,7 +2063,7 @@ object TranslationHelper {
       true

     }

   }

-  

+

   def Version(expr: Expression, etran: ExpressionTranslator): Boogie.Expr =  

   { 

     expr match{

@@ -2318,7 +2318,7 @@ object TranslationHelper {
     }

     replaceThis(expr)

   }

-  

+

   def manipulate(expr: Expression, func: Expression => Expression): Expression = {

     val result = expr match {

       case e: Literal => expr

diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el
index dc3d469c..34a95a87 100644
--- a/Util/Emacs/chalice-mode.el
+++ b/Util/Emacs/chalice-mode.el
@@ -38,7 +38,7 @@
         "above" "acc" "acquire" "and" "assert" "assigned" "assume"

         "below" "between" "call" "credit"

         "downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds"

-        "if" "in" "ite" "join" "lock" "lockbottom" "maxlock" "module" "new" "nil"

+        "if" "in" "ite" "join" "lock" "lockbottom" "waitlevel" "module" "new" "nil"

         "old" "rd" "receive" "release" "reorder" "result" "send" "share"

         "this" "unfold" "unfolding" "unshare" "while"

         "false" "true" "null")) . font-lock-keyword-face)

diff --git a/Util/latex/chalice.sty b/Util/latex/chalice.sty
index f9ba5234..4ef98f9c 100644
--- a/Util/latex/chalice.sty
+++ b/Util/latex/chalice.sty
@@ -22,7 +22,7 @@
     if,in,int,invariant,ite,%

     join,%

     lock,lockbottom,lockchange,%

-    maxlock,method,module,%

+    method,module,%

     new,nil,null,%

     old,%

     predicate,%

@@ -31,7 +31,7 @@
     this,token,true,%

     unfold,unfolding,unshare,%

     var,%

-    while},

+    waitlevel,while},

   literate=%

     {=}{{=~}}1%

     {+=}{{+}{=}~}3%