diff options
author | akashlal <unknown> | 2010-11-23 07:06:26 +0000 |
---|---|---|
committer | akashlal <unknown> | 2010-11-23 07:06:26 +0000 |
commit | 6de6a788ea56b36b802e7b44fe67199c3b7b7e53 (patch) | |
tree | 472a1e8d9bb73dab52e724475d8389991dff571a /Source/VCGeneration/ConditionGeneration.cs | |
parent | fd9227b188714c56402024a42b5d07e7d73d8fbc (diff) |
Refactoring: pulled out all code for stratified inlining to a new file.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 30 |
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
|