commented calls to GC.Collect()

5 files changed, 14 insertions, 8 deletions

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index c8300189..67fbfdb8 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -218,7 +218,7 @@ namespace BytecodeTranslator {
         }

         var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;

         // The decompiler does not turn calls to Assert/Assume into Code Model nodes

-        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);

+        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(m2);

         decompiledModules.Add(m2);

         host.RegisterAsLatest(m2);

         contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 7b5576c1..4073c722 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -444,6 +444,9 @@ namespace Microsoft.Boogie {
         foreach (var x in outcome.assignment) {

           Console.WriteLine(x.Key + " = " + x.Value);

         }

+        if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);

+        }

         errorCount = outcome.ErrorCount;

         verified = outcome.Verified;

         inconclusives = outcome.Inconclusives;

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 645cdee5..c7950c9a 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -585,7 +585,6 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
   | { Spec<pre, mods, post> }

     ImplBody<out locals, out stmtList>

     (.

-      // here we attach kv only to the Procedure, not its implementation

       impl = new Implementation(x, x.val, typeParams,

                                 Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);

     .)

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 3cb27e14..b0c8fabf 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -18,6 +18,7 @@ using VC;
 

 namespace Microsoft.Boogie.Houdini {

   public class HoudiniSession {

+    public static double proverTime = 0;

     private string descriptiveName;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

@@ -49,10 +50,13 @@ namespace Microsoft.Boogie.Houdini {
     public ProverInterface.Outcome Verify(Checker checker, VCExpr axiom, out List<Counterexample> errors) {

       collector.examples.Clear();

       VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);

+

+      DateTime now = DateTime.Now;

       checker.BeginCheck(descriptiveName, vc, handler);

       WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });

-

       ProverInterface.Outcome proverOutcome = checker.ReadOutcome();

+      proverTime += (DateTime.Now - now).TotalSeconds;

+

       if (proverOutcome == ProverInterface.Outcome.Invalid) {

         Contract.Assume(collector.examples != null);

         if (collector.examples.Count == 0) {

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 06fd5502..27b8d05f 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -686,7 +686,7 @@ namespace Microsoft.Boogie.Houdini {
       this.NotifyStart(program, houdiniConstants.Keys.Count);

 

       while (current.WorkList.Count > 0) {

-        System.GC.Collect();

+        //System.GC.Collect();

         this.NotifyIteration();

 

         VCExpr axiom = BuildAxiom(current.Assignment);

@@ -722,7 +722,7 @@ namespace Microsoft.Boogie.Houdini {
 

       while (current.WorkList.Count > 0) {

         bool exceptional = false;

-        System.GC.Collect();

+        //System.GC.Collect();

         this.NotifyIteration();

 

         current.Implementation = current.WorkList.Peek();

@@ -763,7 +763,7 @@ namespace Microsoft.Boogie.Houdini {
 

       while (current.WorkList.Count > 0) {

         bool exceptional = false;

-        System.GC.Collect();

+        //System.GC.Collect();

         this.NotifyIteration();

 

         current.Implementation = current.WorkList.Peek();

@@ -960,7 +960,7 @@ namespace Microsoft.Boogie.Houdini {
 

         do {

           if (pastFirstIter) {

-            System.GC.Collect();

+            //System.GC.Collect();

             this.NotifyIteration();

           }

 

@@ -1027,7 +1027,7 @@ namespace Microsoft.Boogie.Houdini {
           outcome = ProverInterface.Outcome.Undetermined;

 

           if (pastFirstIter) {

-            System.GC.Collect();

+            //System.GC.Collect();

             this.NotifyIteration();

           }