From cd2f64757c0287af4533ed22e1b2421c7b3f09b1 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Mon, 1 Oct 2012 15:59:57 +0200
Subject: Chalice: Disallow unfolding expressions in postconditions.

---
 Chalice/src/main/scala/Resolver.scala | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index 3e4e882b..5dc24662 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -268,6 +268,14 @@ object Resolver {
                }
                b
              }
+             def hasUnfoldingExpression(e: Expression) = {
+               var b = false
+               e visit {
+                 case Unfolding(pred, e) => b = true
+                 case _ =>
+               }
+               b
+             }
              spec foreach {
                case p@Precondition(e) =>
                  ResolveExpr(e, context, false, true)(false)
@@ -276,6 +284,8 @@ object Resolver {
                  ResolveExpr(e, context, false, true)(false)
                  if (hasCredit(e)) context.Error(p.pos, "the specification of functions cannot contain credit expressions") 
                  if (hasAccessibilityPredicate(e)) context.Error(p.pos, "the postcondition of functions cannot contain accessibility predicates (permissions are returned automatically)") 
+                 // The following check is necessary, because the postcondition axiom has the limited function as a trigger.  If we were to allow unfolding expressions, then this might introduce a matching loop.  Since we don't know of any cases where one would use an unfolding expression in the postcondition, we forbid it here.
+                 if (hasUnfoldingExpression(e)) context.Error(p.pos, "the postcondition of functions cannot contain unfolding expressions at the moment") 
                case lc : LockChange => context.Error(lc.pos, "lockchange not allowed on function") 
              }
 
-- 
cgit v1.2.3