diff options
Diffstat (limited to 'Chalice/src/Translator.scala')
| -rw-r--r-- | Chalice/src/Translator.scala | 1 |
1 files changed, 1 insertions, 0 deletions
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
|