From 6de6a788ea56b36b802e7b44fe67199c3b7b7e53 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Tue, 23 Nov 2010 07:06:26 +0000
Subject: Refactoring: pulled out all code for stratified inlining to a new
 file.

---
 Source/VCGeneration/ConditionGeneration.cs | 30 ------------------------------
 1 file changed, 30 deletions(-)

(limited to 'Source/VCGeneration/ConditionGeneration.cs')

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
-- 
cgit v1.2.3