diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-11-09 17:51:47 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-11-09 17:51:47 -0800 |
| commit | 4b18a65874f9e8d4c7ea042f22f7b57c512c6c71 (patch) | |
| tree | 012ee93d15116007fb32835ec26249c7f63e3d13 /Source/Dafny | |
| parent | cea05485e8f58b1831bc5a1c68178164927f1c5b (diff) | |
Dafny: allow assert/assume expressions in more places
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c7fb8481..df2d2b0b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3027,6 +3027,12 @@ namespace Microsoft.Dafny { Error(expr, "allocated expressions are allowed only in specification and ghost contexts");
return;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ // ignore the guard
+ CheckIsNonGhost(e.Body);
+ return;
+
} else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
switch (e.ResolvedOp) {
|