From bdaa9996170aed0b2638962014fe80777b98d5c7 Mon Sep 17 00:00:00 2001
From: jansmans <unknown>
Date: Fri, 2 Oct 2009 15:00:11 +0000
Subject: - where clauses are now properly type-checked - all credits must be
 consumed on entry to a loop by the invariant (to avoid getting the wrong
 maxlock)

---
 Chalice/src/Resolver.scala   | 6 ++++--
 Chalice/src/Translator.scala | 1 +
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 15ed531e..f592740d 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -75,7 +75,7 @@ object Resolver {
       case ch: Channel =>
         for (v <- ch.parameters) {
           ResolveType(v.t, contextNoCurrentClass)
-	}
+	    }
       case cl: Class =>
         for (m <- cl.asInstanceOf[Class].members) m match {
           case _:MonitorInvariant =>
@@ -102,11 +102,13 @@ object Resolver {
     //  * VariableExpr and FieldSelect expressions
     for (decl <- prog) decl match {
       case ch: Channel =>
-        var ctx = new ProgramContext(decls, ChannelClass(ch))
+	    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) {
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 50ffca51..46805d59 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -853,6 +853,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.")) :::
     // save values of local-variable loop targets
     (for (sv <- saveLocalsV) yield BLocal(Variable2BVarWhere(sv))) :::
     (for ((v,sv) <- w.LoopTargetsList zip saveLocalsV) yield
-- 
cgit v1.2.3