minor changes to summary computation

1 files changed, 14 insertions, 3 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 924d5a3b..e6e6eb39 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -331,7 +331,7 @@ namespace VC
                 this.fullyInlinedCache = new HashSet<string>();

                 this.trueSummaryConst = new HashSet<VCExprVar>();

                 this.trueSummaryConstUndeBound = new HashSet<VCExprVar>();

-                this.ComputeUnderBound = ComputeUnderBound;

+                this.ComputeUnderBound = false;

             }

 

             public void boundChanged()

@@ -340,7 +340,7 @@ namespace VC
                 {

                     var s = "";

                     trueSummaryConstUndeBound.Iter(v => s = s + v.ToString() + ",");

-                    Console.WriteLine("Clearing summaries: {{0}}", s);

+                    Console.WriteLine("Clearing summaries: {0}", s);

 

                     // start from scratch

                     trueSummaryConst.ExceptWith(trueSummaryConstUndeBound);

@@ -350,6 +350,11 @@ namespace VC
 

             public void compute(HashSet<int> goodCandidates, int bound)

             {

+                var start = DateTime.Now;

+                goodCandidates = calls.currCandidates;

+

+                var found = 0;

+

                 // Find all nodes that have children only in goodCandidates

                 var overApproxNodes = FindNodes(calls.candidateParent, calls.currCandidates, goodCandidates);

                 overApproxNodes.IntersectWith(calls.summaryCandidates.Keys);

@@ -411,7 +416,8 @@ namespace VC
                             checker2.Pop();

                             if (outcome == Outcome.Correct)

                             {

-                                Console.WriteLine("Found summary: {0}", tup.Item1);

+                                //Console.WriteLine("Found summary: {0}", tup.Item1);

+                                found++;

                                 trueSummaryConst.Add(tup.Item1);

                                 if (usesBound.Contains(cid)) trueSummaryConstUndeBound.Add(tup.Item1);

                             }

@@ -420,6 +426,11 @@ namespace VC
                     checker2.Pop();

                 }

                 checker2.Pop();

+

+                var end = DateTime.Now;

+                Console.WriteLine("Summary computation took {0} sec and inferred {1} of {2} contracts", 

+                    (end - start).TotalSeconds, found, calls.allSummaryConst.Count);

+

             }