diff options
author | akashlal <unknown> | 2010-12-01 17:20:02 +0000 |
---|---|---|
committer | akashlal <unknown> | 2010-12-01 17:20:02 +0000 |
commit | 53d6fccf747dd3592913382c2a773f5390541977 (patch) | |
tree | 9e432635967335cf0f4007dd988f677fd1e1a6dd /Source | |
parent | 6dab818c2ee2e02333b1a6abd1f1ac473846f9b5 (diff) |
stratified inlining: small fix
Diffstat (limited to 'Source')
-rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 75039e4f..d0e3bf2e 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -365,7 +365,6 @@ namespace VC addEdge(0, n);
}
calls.recentlyAddedCandidates = new HashSet<int>();
- syncGraph();
}
public void addEdge(int src_id, int tgt_id)
@@ -910,7 +909,6 @@ namespace VC }
}
DoExpansion(incrementalSearch, toExpand, vState);
- coverageManager.syncGraph();
}
#endregion
@@ -931,7 +929,6 @@ namespace VC if (toExpand.Count == 0) expand = false;
else DoExpansion(incrementalSearch, toExpand, vState);
}
- coverageManager.syncGraph();
}
#endregion
@@ -1009,12 +1006,6 @@ namespace VC done = 1;
coverageManager.reportCorrect();
}
- else if (ret == Outcome.ReachedBound && bound > CommandLineOptions.Clo.RecursionBound)
- {
- // Correct under bound
- done = 1;
- coverageManager.reportCorrect(bound);
- }
else if (ret == Outcome.ReachedBound)
{
// Increment bound
@@ -1026,6 +1017,14 @@ namespace VC if (rb < minRecReached) minRecReached = rb;
}
bound = minRecReached;
+
+ if (bound > CommandLineOptions.Clo.RecursionBound)
+ {
+ // Correct under bound
+ done = 1;
+ coverageManager.reportCorrect(bound);
+ }
+
}
else
{
@@ -1078,7 +1077,8 @@ namespace VC if (PersistCallTree)
{
callTree = new Dictionary<string, int>();
- foreach (var id in calls.candidateParent.Keys)
+ var persistentNodes = new HashSet<int>(calls.candidateParent.Values);
+ foreach (var id in persistentNodes)
{
callTree.Add(calls.getPersistentId(id), 0);
}
|