From 4d7d8d1fc7fce9a18bc3dd0b553427eb8951f6c8 Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Fri, 20 Aug 2010 16:01:24 +0000
Subject: Boogie: Fixed some doubly-inherited-contract occurrences.

---
 Source/Provers/Simplify/Prover.cs          |  8 ++++----
 Source/Provers/Simplify/ProverInterface.cs | 26 +++++++++++++-------------
 2 files changed, 17 insertions(+), 17 deletions(-)

(limited to 'Source')

diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs
index b323b9b8..b789e588 100644
--- a/Source/Provers/Simplify/Prover.cs
+++ b/Source/Provers/Simplify/Prover.cs
@@ -480,7 +480,7 @@ namespace Microsoft.Boogie.Simplify {
     }
 
     public override void AddAxioms(string s) {
-      Contract.Requires(s != null);
+      //Contract.Requires(s != null);
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
       //ToWriteLine("(PROMPT_OFF)");
       base.AddAxioms(s);
@@ -489,7 +489,7 @@ namespace Microsoft.Boogie.Simplify {
     }
 
     public override void Feed(string s, int statementCount) {
-      Contract.Requires(s != null);
+      //Contract.Requires(s != null);
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
       //ToWriteLine("(PROMPT_OFF)");
       base.Feed(s, statementCount);
@@ -506,7 +506,7 @@ namespace Microsoft.Boogie.Simplify {
     }
 
     protected override void DoBeginCheck(string descriptiveName, string formula) {
-      Contract.Requires(descriptiveName != null);
+      //Contract.Requires(descriptiveName != null);
       Contract.Requires(formula != null);
       //simplify.Refresh();
       //this.Comment("@@@@ Virtual Memory:  " + simplify.PeakVirtualMemorySize64);
@@ -518,7 +518,7 @@ namespace Microsoft.Boogie.Simplify {
     }
 
     public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
-      Contract.Requires(handler != null);
+      //Contract.Requires(handler != null);
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
       ProverOutcome outcome;
 
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index ed2402b1..d300a685 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -108,7 +108,7 @@ namespace Microsoft.Boogie.Simplify {
     /// the comment (like, perhaps, a newline or "*/").
     /// </summary>    
     public override void LogComment(string comment) {
-      Contract.Requires(comment != null);
+      //Contract.Requires(comment != null);
       LogComment(comment, false);
     }
 
@@ -326,12 +326,12 @@ namespace Microsoft.Boogie.Simplify {
     /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
     /// </summary>
     public override void PushVCExpression(VCExpr vc) {
-      Contract.Requires(vc != null);
+      //Contract.Requires(vc != null);
       vcExprTranslator.AddAxiom(vcExprTranslator.translate(vc, 1));
     }
 
     public override string VCExpressionToString(VCExpr vc) {
-      Contract.Requires(vc != null);
+      //Contract.Requires(vc != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       return vcExprTranslator.translate(vc, 1);
@@ -382,8 +382,8 @@ namespace Microsoft.Boogie.Simplify {
     private UnexpectedProverOutputException proverException;
 
     public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {
-      Contract.Requires(descriptiveName != null);
-      Contract.Requires(vc != null);
+      //Contract.Requires(descriptiveName != null);
+      //Contract.Requires(vc != null);
       Contract.Requires(handler != null);
       this.NewProblem(descriptiveName);
       this.proverException = null;
@@ -424,7 +424,7 @@ namespace Microsoft.Boogie.Simplify {
     }
 
     public override Outcome CheckOutcome(ErrorHandler handler) {
-      Contract.Requires(handler != null);
+      //Contract.Requires(handler != null);
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
 
       if (this.thmProver == null) {
@@ -613,14 +613,14 @@ namespace Microsoft.Boogie.Simplify {
     }
 
     protected override ProverProcess CreateProverProcess(string proverPath) {
-      Contract.Requires(proverPath != null);
+      //Contract.Requires(proverPath != null);
       Contract.Ensures(Contract.Result<ProverProcess>() != null);
 
       return new SimplifyProverProcess(proverPath);
     }
 
     protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
-      Contract.Requires(opts!=null);
+      //Contract.Requires(opts!=null);
       Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
 
       return new SimplifyVCExprTranslator(gen);
@@ -754,14 +754,14 @@ namespace Microsoft.Boogie.Simplify {
 
 
     public override string Lookup(VCExprVar var) {
-      Contract.Requires(var != null);
+      //Contract.Requires(var != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       return Namer.Lookup(var);
     }
 
     public override string translate(VCExpr expr, int polarity) {
-      Contract.Requires(expr != null);
+      //Contract.Requires(expr != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen);
@@ -813,8 +813,8 @@ namespace Microsoft.Boogie.Simplify {
 
   public class Factory : ProverFactory {
     public override object SpawnProver(ProverOptions options, object ctxt) {
-      Contract.Requires(options != null);
-      Contract.Requires(ctxt != null);
+      //Contract.Requires(options != null);
+      //Contract.Requires(ctxt != null);
       Contract.Ensures(Contract.Result<object>() != null);
 
       return new SimplifyTheoremProver(options,
@@ -823,7 +823,7 @@ namespace Microsoft.Boogie.Simplify {
     }
 
     public override object NewProverContext(ProverOptions options) {
-      Contract.Requires(options != null);
+      //Contract.Requires(options != null);
       Contract.Ensures(Contract.Result<object>() != null);
 
       if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
-- 
cgit v1.2.3