diff options
| author |  stefanheule <unknown> | 2012-02-25 03:32:51 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:32:51 -0800 |
| commit | 2d09a06067320fc7c01d4b6f41a68ac41ddbebe0 (patch) | |
| tree | 891b2ac46ac5377d1b3ddd97a7a5af24bcb3b294 /Chalice/src/main | |
| parent | da27d0eb253f2a9bea48b6da904367792aa927b3 (diff) | |
Chalice: Handle unfolding in function preconditions.
Diffstat (limited to 'Chalice/src/main')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index 887634dc..c2019b12 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -2846,6 +2846,8 @@ object TranslationHelper { combine(functionDependencies(e0, etran), functionDependencies(e1, etran))
case IfThenElse(con, then, els) =>
heapFragment(Boogie.Ite(etran.Tr(con), functionDependencies(then, etran), functionDependencies(els, etran)))
+ case Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), e) =>
+ combine(heapFragment(new Boogie.MapSelect(etran.Heap, etran.Tr(pred.e), pred.predicate.FullName)), functionDependencies(e, etran))
case _: PermissionExpr => throw new InternalErrorException("unexpected permission expression")
case e =>
e visit {_ match { case _ : PermissionExpr => throw new InternalErrorException("unexpected permission expression"); case _ =>}}
@@ -2880,6 +2882,8 @@ object TranslationHelper { functionDependenciesEqual(e0, etran1, etran2) && functionDependenciesEqual(e1, etran1, etran2)
case IfThenElse(con, then, els) =>
functionDependenciesEqual(then, etran1, etran2) && functionDependenciesEqual(els, etran1, etran2)
+ case Unfolding(acc@Access(pred@MemberAccess(obj, f), perm), e) =>
+ (etran1.Heap.select(etran1.Tr(pred.e), pred.predicate.FullName) ==@ etran2.Heap.select(etran2.Tr(pred.e), pred.predicate.FullName)) && functionDependenciesEqual(e, etran1, etran2)
case _: PermissionExpr => throw new InternalErrorException("unexpected permission expression")
case e =>
e visit {_ match { case _ : PermissionExpr => throw new InternalErrorException("unexpected permission expression"); case _ =>}}
|