diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 52bc87ac..320a096a 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1961,9 +1961,6 @@ namespace Microsoft.Dafny }
}
}
- if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {
- Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");
- }
} else if (member is Function) {
var f = (Function)member;
var errorCount = ErrorCount;
@@ -4843,8 +4840,12 @@ namespace Microsoft.Dafny ResolveAttributes(s.Decreases.Attributes, new ResolveOpts(codeContext, true));
foreach (Expression e in s.Decreases.Expressions) {
ResolveExpression(e, new ResolveOpts(codeContext, true));
- if (bodyMustBeSpecOnly && e is WildcardExpr) {
- Error(e, "'decreases *' is not allowed on ghost loops");
+ if (e is WildcardExpr) {
+ if (bodyMustBeSpecOnly) {
+ Error(e, "'decreases *' is not allowed on ghost loops");
+ } else if (!codeContext.AllowsNontermination) {
+ Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
+ }
}
// any type is fine
}
@@ -4877,8 +4878,12 @@ namespace Microsoft.Dafny foreach (Expression e in s.Decreases.Expressions) {
ResolveExpression(e, new ResolveOpts(codeContext, true));
- if (s.IsGhost && e is WildcardExpr) {
- Error(e, "'decreases *' is not allowed on ghost loops");
+ if (e is WildcardExpr) {
+ if (s.IsGhost) {
+ Error(e, "'decreases *' is not allowed on ghost loops");
+ } else if (!codeContext.AllowsNontermination) {
+ Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
+ }
}
// any type is fine
}
@@ -5454,7 +5459,7 @@ namespace Microsoft.Dafny s.Method = (Method)member;
callee = s.Method;
if (!isInitCall && callee is Constructor) {
- Error(s, "a constructor is only allowed to be called when an object is being allocated");
+ Error(s, "a constructor is allowed to be called only when an object is being allocated");
}
s.IsGhost = callee.IsGhost;
if (specContextOnly && !callee.IsGhost) {
@@ -5579,6 +5584,9 @@ namespace Microsoft.Dafny }
}
}
+ if (callee != null && Contract.Exists(callee.Decreases.Expressions, e => e is WildcardExpr) && !codeContext.AllowsNontermination) {
+ Error(s.Tok, "a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating");
+ }
}
/// <summary>
|