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 | |
| parent | cea05485e8f58b1831bc5a1c68178164927f1c5b (diff) | |
Dafny: allow assert/assume expressions in more places
| -rw-r--r-- | Source/Dafny/Resolver.cs | 6 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/PredExpr.dfy | 8 |
3 files changed, 15 insertions, 1 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) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index bcdb7126..3198df33 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1321,4 +1321,4 @@ PredExpr.dfy(36,17): Error: condition in assert expression might not hold Execution trace:
(0,0): anon0
-Dafny program verifier finished with 7 verified, 2 errors
+Dafny program verifier finished with 9 verified, 2 errors
diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy index 3499a01c..740c2308 100644 --- a/Test/dafny0/PredExpr.dfy +++ b/Test/dafny0/PredExpr.dfy @@ -41,3 +41,11 @@ method M1(j: int) returns (n: nat) n := (assume 0 <= j; j) + (assert 0 <= j; j);
assert n == 2*j;
}
+
+function SpecOnly(): bool { true }
+
+function method FuncMeth(): int {
+ assert SpecOnly(); // this call is allowed, because the .Guard of a
+ // PredicateExpr is not included in compilation
+ 15
+}
|