diff options
| author |  akashlal <unknown> | 2010-11-14 05:37:39 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-11-14 05:37:39 +0000 |
| commit | 20ff8028079c6a7c5b4eb2999d1cad98c51ec5bb (patch) | |
| tree | 42f7f38713c44c6943d45719e72c6258a30ba4cc | |
| parent | b58a9b7eb18081726921c5e9ff41991992aafb0d (diff) | |
Minor updates for printing coverage graph of stratified inlining
| -rw-r--r-- | Source/VCGeneration/VC.cs | 41 |
1 files changed, 39 insertions, 2 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 9e8b2dc8..bfbea10c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2069,7 +2069,7 @@ namespace VC { {
var pid = calls.candidateParent[id];
var str = calls.getPersistentName(pid);
- coverageProcess.StandardInput.WriteLine("color " + str);
+ coverageProcess.StandardInput.WriteLine("color green " + str);
}
}
}
@@ -2257,9 +2257,46 @@ namespace VC { Console.WriteLine("Stratified Inlining: VC Size: {0}", vcSize);
}
+ if (coverageProcess != null)
+ {
+ coverageProcess.StandardInput.WriteLine("reset_graph_round");
+ // Go through the curr candidates and write down their parents (i.e.,
+ // those procedures that have an assume false in them)
+ var colorRed = new Set();
+ var colorOrange = new Set();
+ foreach (var id in calls.currCandidates)
+ {
+ if (calls.candidateParent.ContainsKey(id))
+ {
+ var pid = calls.candidateParent[id];
+ var str = calls.getPersistentName(pid);
+ if (calls.getRecursionBound(id) > CommandLineOptions.Clo.RecursionBound)
+ {
+ colorOrange.Remove(str);
+ colorRed.Add(str);
+ }
+ else
+ {
+ if (!colorRed.Contains(str)) colorOrange.Add(str);
+ }
+
+ }
+ }
+
+ foreach (var str in colorOrange)
+ {
+ coverageProcess.StandardInput.WriteLine("color orange " + str.ToString());
+ }
+
+ foreach (var str in colorRed)
+ {
+ coverageProcess.StandardInput.WriteLine("color red " + str.ToString());
+ }
+ }
+
if (coverageProcess != null && stopCoverageProcess)
{
- coverageProcess.StandardInput.WriteLine("Done");
+ coverageProcess.StandardInput.WriteLine("AllDone");
do
{
|