diff options
-rw-r--r-- | Chalice/src/main/scala/Resolver.scala | 10 |
1 files changed, 10 insertions, 0 deletions
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")
}
|