Removed program argument from VerifyImplementation. It is redundant since the constructor of ConditionGeneration

takes a program reference and stashes it in a field.

5 files changed, 29 insertions, 24 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 0911cbd3..44adce15 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -701,7 +701,7 @@ namespace Microsoft.Boogie {
               Console.WriteLine();

             }

             else {

-              outcome = vcgen.VerifyImplementation(impl, program, out errors);

+              outcome = vcgen.VerifyImplementation(impl, out errors);

               if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) {

                 for (int i = 0; i < errors.Count; i++) {

                   errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index dd898c36..ba58a5de 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -447,9 +447,8 @@ namespace VC {
   }

   [ContractClassFor(typeof(ConditionGeneration))]

   public abstract class ConditionGenerationContracts : ConditionGeneration {

-    public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {

+    public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {

       Contract.Requires(impl != null);

-      Contract.Requires(program != null);

       Contract.Requires(callback != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

@@ -522,9 +521,8 @@ namespace VC {
     /// each counterexample consisting of an array of labels.

     /// </summary>

     /// <param name="impl"></param>

-    public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {

+    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample>/*?*/ errors) {

       Contract.Requires(impl != null);

-      Contract.Requires(program != null);

 

       Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

       Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);

@@ -532,7 +530,7 @@ namespace VC {
       Helpers.ExtraTraceInformation("Starting implementation verification");

 

       CounterexampleCollector collector = new CounterexampleCollector();

-      Outcome outcome = VerifyImplementation(impl, program, collector);

+      Outcome outcome = VerifyImplementation(impl, collector);

       if (outcome == Outcome.Errors) {

         errors = collector.examples;

       } else {

@@ -550,7 +548,7 @@ namespace VC {
     /// each counterexample consisting of an array of labels.

     /// </summary>

     /// <param name="impl"></param>

-    public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<Model> errorsModel)

+    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample> errors, out List<Model> errorsModel)

     {

         Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null);

         Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

@@ -558,14 +556,14 @@ namespace VC {
 

         Outcome outcome;

         errorModelList = new List<Model>();

-        outcome = VerifyImplementation(impl, program, out errorsOut);

+        outcome = VerifyImplementation(impl, out errorsOut);

         errors = errorsOut;

         errorsModel = errorModelList;

 

         return outcome;

     }

 

-    public abstract Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback);

+    public abstract Outcome VerifyImplementation(Implementation impl, VerifierCallback callback);

 

     /////////////////////////////////// Common Methods and Classes //////////////////////////////////////////

 

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 65aa8486..058b5de9 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -367,10 +367,26 @@ namespace VC {
     private bool useSummary;

     private SummaryComputation summaryComputation;

     private HashSet<string> procsThatReachedRecBound;

-    public int boundUsedInLastQuery { get; private set; }

     public HashSet<string> procsToSkip;

     public Dictionary<string, int> extraRecBound;

 

+    public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree, 

+                           HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,

+                           Program program, string/*?*/ logFilePath, bool appendLogFile) 

+    : this(program, logFilePath, appendLogFile)

+    {

+      this.procsToSkip = new HashSet<string>(procsToSkip);

+      this.extraRecBound = new Dictionary<string, int>(extraRecBound);

+

+      if (usePrevCallTree) {

+        callTree = prevCallTree;

+        PersistCallTree = true;

+      }

+      else {

+        PersistCallTree = false;

+      }

+    }

+

     public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

       : base(program, logFilePath, appendLogFile) {

       this.GenerateRecordFunctions();

@@ -379,7 +395,6 @@ namespace VC {
       procsThatReachedRecBound = new HashSet<string>();

       procsToSkip = new HashSet<string>();

       extraRecBound = new Dictionary<string, int>();

-      boundUsedInLastQuery = -1;

     }

 

     // Is this procedure to be "skipped" 

@@ -1189,7 +1204,7 @@ namespace VC {
       }

     }

 

-    public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {

+    public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {

       Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));

       Debug.Assert(this.program == program);

 

@@ -1318,8 +1333,6 @@ namespace VC {
       //   case 2: (bug)     We find a bug

       //   case 3: (internal error)   The theorem prover TimesOut of runs OutOfMemory

       while (true) {

-        boundUsedInLastQuery = bound;

-

         // Check timeout

         if (CommandLineOptions.Clo.ProverKillTime != -1) {

           if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 7e3e3f17..373b685a 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1384,10 +1384,7 @@ namespace VC {
       }

     }

 

-    public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {

-      //Contract.Requires(impl != null);

-      //Contract.Requires(program != null);

-      //Contract.Requires(callback != null);

+    public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

 

       if (impl.SkipVerification) {

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 4d2e0775..15c6e2aa 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -101,10 +101,7 @@ namespace VC {
     /// - check if |= (reach=false) => wlp.S.false holds for each reach

     ///

     /// </summary>

-    public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {

-      //Contract.Requires(impl != null);

-      //Contract.Requires(program != null);

-      //Contract.Requires(callback != null);

+    public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) {

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       

       Console.WriteLine();

@@ -115,7 +112,7 @@ namespace VC {
 

       //Impl2Dot(impl, String.Format("c:/dot/{0}_orig.dot", impl.Name));      

 

-      Transform4DoomedCheck(impl, program);

+      Transform4DoomedCheck(impl);

 

       //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));

     

@@ -694,7 +691,7 @@ namespace VC {
     // this might be redundant, but I didn't find a better place to get this information.     

     private Dictionary<Variable, Expr> m_LastReachVarIncarnation = new Dictionary<Variable, Expr>();

 

-    private void Transform4DoomedCheck(Implementation impl, Program program)

+    private void Transform4DoomedCheck(Implementation impl)

     {

         variable2SequenceNumber = new Hashtable/*Variable -> int*/();

         incarnationOriginMap = new Dictionary<Incarnation, Absy>();