summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2010-12-01 17:20:02 +0000
committerGravatar akashlal <unknown>2010-12-01 17:20:02 +0000
commit53d6fccf747dd3592913382c2a773f5390541977 (patch)
tree9e432635967335cf0f4007dd988f677fd1e1a6dd /Source
parent6dab818c2ee2e02333b1a6abd1f1ac473846f9b5 (diff)
stratified inlining: small fix
Diffstat (limited to 'Source')
-rw-r--r--Source/VCGeneration/StratifiedVC.cs20
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);
}