diff options
| author |  stefanheule <unknown> | 2012-02-25 03:17:27 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:17:27 -0800 |
| commit | 2d21d5d3a77d82cea4dc663de012f24bcbb80e33 (patch) | |
| tree | ff08f1b4c0dee8339195ae005f7955a9377a9857 /Chalice/src/main | |
| parent | 6bab240caf5964fa1feea137e85b82df48619eae (diff) | |
Chalice: change order of unfold treatment; first inhale predicate body, then exhale predicate
Diffstat (limited to 'Chalice/src/main')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index a4e986a6..163bc42a 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -684,8 +684,9 @@ class Translator { isDefined(e) :::
bassert(nonNull(o), s.pos, "The target of the fold statement might be null.") ::
isDefined(perm) :::
+ etran.Inhale(List(definition), "unfold", false, unfoldK) :::
Exhale(List((acc, ErrorMessage(s.pos, "unfold might fail because the predicate " + pred.predicate.FullName + " does not hold."))), "unfold", unfoldK, false) :::
- etran.Inhale(List(definition), "unfold", false, unfoldK)
+ Nil
case c@CallAsync(declaresLocal, token, obj, id, args) =>
val formalThisV = new Variable("this", new Type(c.m.Parent))
val formalThis = new VariableExpr(formalThisV)
|