diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 9 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 12 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 5 |
3 files changed, 24 insertions, 2 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 61ed3419..f5010443 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3921,7 +3921,14 @@ namespace Microsoft.Dafny { public readonly IToken OpenParen; // can be null if Args.Count == 0
public readonly List<Expression/*!*/>/*!*/ Args;
public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // created, initialized, and used by resolution (and also used by translation)
- public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }
+ public enum CoCallResolution {
+ No,
+ Yes,
+ NoBecauseFunctionHasSideEffects,
+ NoBecauseFunctionHasPostcondition,
+ NoBecauseRecursiveCallsAreNotAllowedInThisContext,
+ NoBecauseIsNotGuarded
+ }
public CoCallResolution CoCall = CoCallResolution.No; // indicates whether or not the call is a co-recursive call; filled in by resolution
[ContractInvariantMethod]
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 762bcc7e..dd59bf57 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -7425,6 +7425,18 @@ namespace Microsoft.Dafny } else {
e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
}
+ } else if (e.Function.Ens.Count != 0) {
+ // this call is disqualified from being a co-call, because it has a postcondition
+ // (a postcondition could be allowed, as long as it does not get to be used with
+ // co-recursive calls, because that could be unsound; for example, consider
+ // "ensures false;")
+ if (!dealsWithCodatatypes) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.No;
+ } else if (coContext != null) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition;
+ } else {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
+ }
} else if (!allowCallsWithinRecursiveCluster) {
if (!dealsWithCodatatypes) {
e.CoCall = FunctionCallExpr.CoCallResolution.No;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index ba993caf..49173230 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3303,7 +3303,10 @@ namespace Microsoft.Dafny { string hint;
switch (e.CoCall) {
case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects:
- hint = "note that only functions without side effects can called co-recursively";
+ hint = "note that only functions without side effects can be called co-recursively";
+ break;
+ case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition:
+ hint = "note that only functions without any ensures clause can be called co-recursively";
break;
case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded:
hint = "note that the call is not sufficiently guarded to be used co-recursively";
|