- 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)

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