Boogie: Simplify: Added a contracts class that I forgot in the initial porting.

1 files changed, 20 insertions, 2 deletions

diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs
index e4a72a89..595560ed 100644
--- a/Source/Provers/Simplify/Prover.cs
+++ b/Source/Provers/Simplify/Prover.cs
@@ -17,6 +17,8 @@ namespace Microsoft.Boogie.Simplify {
   /// <summary>

   /// An interface to Simplify theorem prover.

   /// </summary>

+  /// 

+  [ContractClass(typeof(ProverProcessContracts))]

   public abstract class ProverProcess {

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -413,7 +415,24 @@ namespace Microsoft.Boogie.Simplify {
       cce.EndExpose();

     }

   }

+  [ContractClassFor(typeof(ProverProcess))]

+  public abstract class ProverProcessContracts : ProverProcess {

+    public override string OptionComments() {

+      Contract.Ensures(Contract.Result<string>() != null);

+      throw new NotImplementedException();

+    }

 

+    public override ProverProcess.ProverOutcome CheckOutcome(ProverInterface.ErrorHandler handler) {

+      Contract.Requires(handler != null);

+      throw new NotImplementedException();

+    }

+

+    protected override void DoBeginCheck(string descriptiveName, string formula) {

+      Contract.Requires(descriptiveName != null);

+      Contract.Requires(formula != null);

+      throw new NotImplementedException();

+    }

+  }

   // derived by Z3ProverProcess

   public class SimplifyProverProcess : ProverProcess {

     public SimplifyProverProcess(string proverPath, bool dummy) :base(getPSI(proverPath),proverPath) {

@@ -629,5 +648,4 @@ namespace Microsoft.Boogie.Simplify {
     }

   }

 

-}

-

+}
\ No newline at end of file