diff options
| author |  stefanheule <unknown> | 2012-10-01 15:56:23 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-10-01 15:56:23 +0200 |
| commit | f37284c3d961cd3d53858a814f9e03a4f40859c0 (patch) | |
| tree | 256e652f6297b0f42f8acdd3a6e801183133fc55 /Chalice | |
| parent | 1834b06f39ee460a36831bf5047fe77d9edff3db (diff) | |
Chalice: Fix bug in detecting permissions in postconditions.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/main/scala/Resolver.scala | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala index 3acd2499..3e4e882b 100644 --- a/Chalice/src/main/scala/Resolver.scala +++ b/Chalice/src/main/scala/Resolver.scala @@ -260,10 +260,11 @@ object Resolver { }
def hasAccessibilityPredicate(e: Expression) = {
var b = false
- e transform {
- case _: PermissionExpr => b = true; None
- case ma: MemberAccess => if (ma.isPredicate) b = true; None
- case _ => None
+ e visitOpt {
+ case _: PermissionExpr => b = true; false
+ case ma: MemberAccess => if (ma.isPredicate) { b = true; false } else { true }
+ case Unfolding(pred, e) => false
+ case _ => true
}
b
}
|