From 88cf411f8a95912749c7402d1cddd0b5a3f87e73 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Sun, 20 May 2012 17:51:24 +0200
Subject: Chalice: Remove some old code updating the secondary mask, and add a
 missing well-formed assumption.

---
 Chalice/src/main/scala/Translator.scala | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'Chalice')

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index 85ae2ec0..7f500eb9 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -1659,15 +1659,12 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         tmpTranslator.ExhaleDuringUnfold(List((acc, ErrorMessage(unfolding.pos, "Unfolding might fail."))), "unfolding", false, unfoldingK, false) :::
         // inhale the definition of the predicate
         tmpTranslator.Inhale(List(definition), "unfolding", false, unfoldingK) :::
-        // remove secondary permissions (if any), and add them again
-        (if (isOldEtran) Nil else
-          UpdateSecMaskDuringUnfold(pred.predicate, Tr(obj), Heap.select(Tr(obj), pred.predicate.FullName), perm, unfoldingK) :::
-          TransferPermissionToSecMask(pred.predicate, obj, perm, unfolding.pos)) :::
         // update the predicate mask to indicate the predicates that are folded under 'pred'
         (if (isOldEtran) Nil
         else etran.keepFoldedLocations(definition, o, pred.predicate, etran.Mask, etran.Heap, etran.fpi.getFoldedPredicates(pred.predicate))) :::
         // check definedness of e in state where the predicate is unfolded
-        tmpTranslator.isDefined(e)
+        tmpTranslator.isDefined(e) :::
+        bassume(wf(etran.Heap, etran.Mask, etran.SecMask)) :: Nil
         
         // record folded predicate
         val version = Heap.select(o, pred.predicate.FullName)
-- 
cgit v1.2.3