diff options
| -rw-r--r-- | Chalice/src/Resolver.scala | 6 | ||||
| -rw-r--r-- | 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
|