diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-06-29 12:40:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-06-29 12:40:57 -0700 |
| commit | 72799f600cc520253f0fc26a0327466bbaa28903 (patch) | |
| tree | 5580bddeaeb4ffeb1b049b32ad436e03ba454ac1 /Source/Dafny/Resolver.cs | |
| parent | 141863d4677fc7bd7b2c6891d6f354b7d9237036 (diff) | |
Fixed soundness bug with co-recursive calls: co-recursive calls may now no longer to to functions with ensures clauses
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;
|