Boogie: Fixed some doubly-inherited-contract occurrences.

3 files changed, 75 insertions, 75 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 4b4d7431..926624b4 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -85,9 +85,9 @@ void ObjectInvariant()
     }}

 

     public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {

-      Contract.Requires(descriptiveName != null);

-      Contract.Requires(vc != null);

-      Contract.Requires(handler != null);

+      //Contract.Requires(descriptiveName != null);

+      //Contract.Requires(vc != null);

+      //Contract.Requires(handler != null);

       TextWriter output = OpenOutputFile(descriptiveName);

       Contract.Assert(output!=null);

 

@@ -157,7 +157,7 @@ void ObjectInvariant()
 

     [NoDefaultContract]

     public override Outcome CheckOutcome(ErrorHandler handler)

-   {Contract.Requires(handler != null);

+   {  //Contract.Requires(handler != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       return Outcome.Undetermined;

     }

@@ -263,8 +263,8 @@ void ObjectInvariant()
 

     public override object SpawnProver(ProverOptions options, object ctxt)

     {

-    Contract.Requires(ctxt != null);

-    Contract.Requires(options != null);

+    //Contract.Requires(ctxt != null);

+    //Contract.Requires(options != null);

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

 

       return this.SpawnProver(options,

@@ -273,7 +273,7 @@ void ObjectInvariant()
     }

 

     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) {

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 73ae55a9..281d36f9 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -228,8 +228,8 @@ void ObjectInvariant()
     /////////////////////////////////////////////////////////////////////////////////////

 

     public bool Visit(VCExprLiteral node, LineariserOptions options) {

-      Contract.Requires(node != null);

-      Contract.Requires(options != null);

+      //Contract.Requires(node != null);

+      //Contract.Requires(options != null);

       if (options.AsTerm) {

 

         if (node == VCExpressionGenerator.True)

@@ -268,8 +268,8 @@ void ObjectInvariant()
     /////////////////////////////////////////////////////////////////////////////////////

 

     public bool Visit(VCExprNAry node, LineariserOptions options) {

-      Contract.Requires(node != null);

-      Contract.Requires(options != null);

+      //Contract.Requires(node != null);

+      //Contract.Requires(options != null);

       

       VCExprOp op = node.Op;

       Contract.Assert(op!=null);

@@ -302,8 +302,8 @@ void ObjectInvariant()
     /////////////////////////////////////////////////////////////////////////////////////

 

     public bool Visit(VCExprVar node, LineariserOptions options) {

-      Contract.Requires(node != null);

-      Contract.Requires(options != null);

+      //Contract.Requires(node != null);

+      //Contract.Requires(options != null);

       string printedName = Namer.GetName(node, MakeIdPrintable(node.Name));

       Contract.Assert(printedName!=null);

 

@@ -320,8 +320,8 @@ void ObjectInvariant()
     /////////////////////////////////////////////////////////////////////////////////////

 

     public bool Visit(VCExprQuantifier node, LineariserOptions options) {

-      Contract.Requires(node != null);

-      Contract.Requires(options != null);

+      //Contract.Requires(node != null);

+      //Contract.Requires(options != null);

       AssertAsFormula(node.Quan.ToString(), options);

      Contract.Assert(node.TypeParameters.Count == 0);

 

@@ -416,8 +416,8 @@ void ObjectInvariant()
     /////////////////////////////////////////////////////////////////////////////////////

 

     public bool Visit(VCExprLet node, LineariserOptions options) {

-      Contract.Requires(node != null);

-      Contract.Requires(options != null);

+      //Contract.Requires(node != null);

+      //Contract.Requires(options != null);

       Namer.PushScope(); try {

 

       foreach (VCExprLetBinding b in node) {

@@ -553,8 +553,8 @@ void ObjectInvariant()
       ///////////////////////////////////////////////////////////////////////////////////

       

       public bool VisitNotOp      (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

         WriteApplication(boolNotName, notName, node, options);      // arguments can be both terms and formulas

         return true;

       }

@@ -595,14 +595,14 @@ void ObjectInvariant()
       }

 

       public bool VisitEqOp       (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

         return PrintEq(node, options);

       }

 

       public bool VisitNeqOp      (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

         wr.Write("({0} ", options.AsTerm ? boolNotName : notName);

         PrintEq(node, options);

         wr.Write(")");

@@ -610,41 +610,41 @@ void ObjectInvariant()
       }

 

       public bool VisitAndOp      (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        Contract.Assert(options.AsTerm);

         WriteApplication(boolAndName, andName, node, options);

         return true;

       }

 

       public bool VisitOrOp       (VCExprNAry node, LineariserOptions options) {

-      Contract.Requires(node != null);

-        Contract.Requires(options != null);

-       

-       Contract.Assert(options.AsTerm);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

+        

+        Contract.Assert(options.AsTerm);

         WriteApplication(boolOrName, orName, node, options);

         return true;

       }

 

       public bool VisitImpliesOp  (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(boolImpliesName, impliesName, node, options);

         return true;

       }

 

       public bool VisitIfThenElseOp  (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(boolIteName, iteName, node, options);

         return true;

       }

 

       public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

 

         VCExprCustomOp op = (VCExprCustomOp)node.Op;

         WriteApplicationTermOnly(op.Name, node, options);

@@ -652,8 +652,8 @@ void ObjectInvariant()
       }

 

       public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         ExprLineariser.AssertAsFormula(distinctName, options);

         

@@ -673,9 +673,9 @@ void ObjectInvariant()
       }

 

       public bool VisitLabelOp    (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

-        Contract.Requires(node.Length>=1);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

+        //Contract.Requires(node.Length>=1);

         // VCExprLabelOp! op = (VCExprLabelOp)node.Op;

         // TODO

         //        wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));

@@ -685,131 +685,131 @@ void ObjectInvariant()
       }

 

       public bool VisitSelectOp   (VCExprNAry node, LineariserOptions options) {

-       Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

        {Contract.Assert(false);  throw new cce.UnreachableException();}      // should not occur in the output

       }

 

       public bool VisitStoreOp    (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

        {Contract.Assert(false);  throw new cce.UnreachableException();}       // should not occur in the output

       }

 

       public bool VisitBvOp       (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

        {Contract.Assert(false);  throw new NotImplementedException();}       // TODO

       }

 

       public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

        {Contract.Assert(false);  throw new NotImplementedException();}       // TODO

       }

 

       public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

        {Contract.Assert(false);  throw new NotImplementedException();}       // TODO

       }

 

       public bool VisitAddOp            (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteTermApplication(intAddName, node, options);

         return true;

       }

 

       public bool VisitSubOp            (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteTermApplication(intSubName, node, options);

         return true;

       }

 

       public bool VisitMulOp            (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteTermApplication(intMulName, node, options);

         return true;

       }

 

       public bool VisitDivOp            (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteTermApplication(intDivName, node, options);

         return true;

       }

 

       public bool VisitModOp            (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteTermApplication(intModName, node, options);

         return true;

       }

 

       public bool VisitLtOp             (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(termLessName, lessName, node, options, true);  // arguments are always terms

         return true;

       }

 

       public bool VisitLeOp             (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(termAtmostName, atmostName, node, options, true);  // arguments are always terms

         return true;

       }

 

       public bool VisitGtOp             (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(termGreaterName, greaterName, node, options, true);  // arguments are always terms

         return true;

       }

 

       public bool VisitGeOp             (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(termAtleastName, atleastName, node, options, true);  // arguments are always terms

         return true;

       }

 

       public bool VisitSubtypeOp        (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(subtypeName, node, options, true);               // arguments are always terms

         return true;

       }

 

       public bool VisitSubtype3Op        (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         WriteApplication(subtypeArgsName, node, options, true);               // arguments are always terms

         return true;

       }

 

       public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options) {

-        Contract.Requires(node != null);

-        Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        //Contract.Requires(options != null);

        

         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

         Contract.Assert(op!=null);

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index a0d56601..2211701c 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -36,7 +36,7 @@ void ObjectInvariant()
 

     // not used

     protected override bool StandardResult(VCExpr node, bool arg) {

-      Contract.Requires(node != null);

+      //Contract.Requires(node != null);

       return true;

     }