diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 0dbf7a27..57527202 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1483,8 +1483,8 @@ namespace Microsoft.Dafny var coCandidates = new List<CoCallResolution.CoCallInfo>();
var hasIntraClusterCallsInDestructiveContexts = false;
foreach (var m in module.CallGraph.GetSCC(fn)) {
- if (m is Function) {
- var f = (Function)m;
+ var f = m as Function;
+ if (f != null && f.Body != null) {
var checker = new CoCallResolution(f, dealsWithCodatatypes);
checker.CheckCoCalls(f.Body);
coCandidates.AddRange(checker.FinalCandidates);
@@ -7922,7 +7922,9 @@ namespace Microsoft.Dafny CheckCoCalls(arg, int.MaxValue, null, coCandidates);
}
// Second, investigate the possibility that this call itself may be a candidate co-call
- if (currentModule.CallGraph.GetSCCRepresentative(currentFunction) == currentModule.CallGraph.GetSCCRepresentative(e.Function)) {
+ var calleeModule = e.Function.EnclosingClass.Module;
+ if (currentModule == calleeModule &&
+ currentModule.CallGraph.GetSCCRepresentative(currentFunction) == calleeModule.CallGraph.GetSCCRepresentative(e.Function)) {
// This call goes to another function in the same recursive cluster
if (destructionLevel > 0) {
// a potentially destructive context
|