diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 22a58a39..972c82ab 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1316,7 +1316,7 @@ namespace Microsoft.Dafny { } else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
- bool bodyIsSpecOnly = specContextOnly;
+ bool bodyMustBeSpecOnly = specContextOnly;
if (s.Guard != null) {
int prevErrorCount = ErrorCount;
ResolveExpression(s.Guard, true, true);
@@ -1326,7 +1326,7 @@ namespace Microsoft.Dafny { Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
}
if (!specContextOnly && successfullyResolved) {
- bodyIsSpecOnly = UsesSpecFeatures(s.Guard);
+ bodyMustBeSpecOnly = UsesSpecFeatures(s.Guard);
}
}
foreach (MaybeFreeExpression inv in s.Invariants) {
@@ -1338,10 +1338,13 @@ namespace Microsoft.Dafny { }
foreach (Expression e in s.Decreases) {
ResolveExpression(e, true, true);
+ if (bodyMustBeSpecOnly && e is WildcardExpr) {
+ Error(e, "'decreases *' is not allowed on ghost loops");
+ }
// any type is fine
}
- s.IsGhost = bodyIsSpecOnly;
- ResolveStatement(s.Body, bodyIsSpecOnly, method);
+ s.IsGhost = bodyMustBeSpecOnly;
+ ResolveStatement(s.Body, bodyMustBeSpecOnly, method);
} else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
|