diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 12 |
1 files changed, 12 insertions, 0 deletions
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;
|