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/Translator.scala | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Chalice/src/Translator.scala')

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