Refactoring: pulled out all code for stratified inlining to a new file.

1 files changed, 0 insertions, 30 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 031f0f18..1a16f11e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -539,38 +539,8 @@ namespace VC {
         return outcome;

     }

   

-

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

-      Contract.Requires(impl != null);

-      Contract.Requires(program != null);

-      Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

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

-      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

-      Helpers.ExtraTraceInformation("Starting implementation verification");

-

-      CounterexampleCollector collector = new CounterexampleCollector();

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

-      if (outcome == Outcome.Errors) {

-        errors = collector.examples;

-      } else {

-        errors = null;

-      }

-

-      Helpers.ExtraTraceInformation("Finished implementation verification");

-      return outcome;

-    }

-

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

 

-    public virtual Outcome StratifiedVerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {

-

-      Contract.Requires(impl != null);

-      Contract.Requires(program != null);

-      Contract.Requires(callback != null);

-      Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

-      return VerifyImplementation(impl, program, callback);

-    }

-

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

 

     #region Methods for injecting pre- and postconditions