Boogie: Fixed some doubly-inherited-contract occurrences.

4 files changed, 29 insertions, 29 deletions

diff --git a/Source/VCExpr/Clustering.cs b/Source/VCExpr/Clustering.cs
index ae22fa7f..0f08c98e 100644
--- a/Source/VCExpr/Clustering.cs
+++ b/Source/VCExpr/Clustering.cs
@@ -52,7 +52,7 @@ namespace Microsoft.Boogie.Clustering {
     ////////////////////////////////////////////////////////////////////////////

 

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

-      Contract.Requires(node != null);

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

       return false;   // by default, do not collect terms containing node

     }

 

@@ -486,8 +486,8 @@ Contract.Ensures(Contract.Result<VCExprVar>() != null);
     }

 

     protected override VCExpr StandardResult(VCExpr node, VCExpr that) {

-      Contract.Requires(that != null);

-      Contract.Requires(node != null);

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

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

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

       Contract.Assert(false);

       throw new cce.UnreachableException(); // not handled here      

@@ -510,8 +510,8 @@ Contract.Ensures(Contract.Result<VCExprVar>() != null);
     }

 

     protected override bool StandardResult(VCExpr node, IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ globalVars) {

-      Contract.Requires(node != null);

-      Contract.Requires(cce.NonNullElements(globalVars));

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

+      //Contract.Requires(cce.NonNullElements(globalVars));

       VCExprVar nodeAsVar = node as VCExprVar;

       if (nodeAsVar == null || globalVars.ContainsKey(nodeAsVar))

         Size = Size + 1;

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index f148dc79..45533115 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -714,7 +714,7 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
     // Type.Int, and Type.Bool

 

     public override Type TypeAfterErasure(Type type) {

-      Contract.Requires(type != null);

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

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

       if (UnchangedType(type))

         // these types are kept

@@ -726,7 +726,7 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
 

     [Pure]

     public override bool UnchangedType(Type type) {

-      Contract.Requires(type != null);

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

       return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);

     }

 

@@ -1142,9 +1142,9 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
 

     // this method is called by MutatingVCExprVisitor.Visit(VCExprNAry, ...)

     protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VariableBindings/*!*/ bindings) {

-      Contract.Requires(originalNode != null);

-      Contract.Requires(cce.NonNullElements(newSubExprs));

-      Contract.Requires(bindings != null);

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

+      //Contract.Requires(cce.NonNullElements(newSubExprs));

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

       Contract.Assume(originalNode.Op == VCExpressionGenerator.AndOp ||

              originalNode.Op == VCExpressionGenerator.OrOp);

       return Gen.Function(originalNode.Op,

@@ -1307,8 +1307,8 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
     }

 

     protected override VCExpr StandardResult(VCExprNAry node, VariableBindings bindings) {

-      Contract.Requires(bindings != null);

-      Contract.Requires(node != null);

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

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

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

       System.Diagnostics.Debug.Fail("Don't know how to erase types in this expression: " + node);

       Contract.Assert(false);

@@ -1570,7 +1570,7 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
     readonly TypeAxiomBuilderIntBoolU/*!*/ AxBuilder;

 

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

-      Contract.Requires(node != null);

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

       return true; // not used

     }

 

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 62bc72ea..c63a158f 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -54,8 +54,8 @@ namespace Microsoft.Boogie.TypeErasure {
     // by the SMT-solver, i.e., that U2Int is only applied to terms that actually

     // are of type int)

     protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) {

-      Contract.Requires(castFromU != null);

-      Contract.Requires(castToU != null);

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

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

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

       List<VCTrigger/*!*/>/*!*/ triggers;

       VCExprVar/*!*/ var;

@@ -64,8 +64,8 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {

-      Contract.Requires(castFromU != null);

-      Contract.Requires(castToU != null);

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

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

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

       // nothing

       return VCExpressionGenerator.True;

@@ -84,8 +84,8 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) {

-      Contract.Requires(originalType != null);

-      Contract.Requires(var != null);

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

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

       // no axioms are needed for variable or function types

     }

 

@@ -171,8 +171,8 @@ namespace Microsoft.Boogie.TypeErasure {
     ////////////////////////////////////////////////////////////////////////////

 

     protected override void GenSelectStoreFunctions(MapType abstractedType, TypeCtorDecl synonym, out Function/*!*/ select, out Function/*!*/ store) {

-      Contract.Requires(((synonym != null)));

-Contract.Requires(((abstractedType != null)));

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

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

 Contract.Ensures(Contract.ValueAtReturn(out select) != null);

 Contract.Ensures(Contract.ValueAtReturn(out store) != null);

       Contract.Assert(synonym.Name != null);

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index c36551d6..09794803 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -99,8 +99,8 @@ void ObjectInvariant()
     // generate axioms of the kind "forall x:U. {Int2U(U2Int(x))}

     //                                          type(x)=int ==> Int2U(U2Int(x))==x"

     protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) {

-      Contract.Requires(castFromU != null);

-      Contract.Requires(castToU != null);

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

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

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

       List<VCTrigger/*!*/>/*!*/ triggers;

       VCExprVar/*!*/ var;

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

 

     protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {

-      Contract.Requires(castFromU != null);

-      Contract.Requires(castToU != null);

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

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

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

       Type/*!*/ fromType = cce.NonNull(castToU.InParams[0]).TypedIdent.Type;

       return GenFunctionAxiom(castToU, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>(),

@@ -485,8 +485,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
     ////////////////////////////////////////////////////////////////////////////

 

     protected override void AddVarTypeAxiom(VCExprVar var, Type originalType){

-Contract.Requires(originalType != null);

-Contract.Requires(var != null);

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

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

       if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) return;

       AddTypeAxiom(GenVarTypeAxiom(var, originalType,

                                    // we don't have any bindings available

@@ -574,8 +574,8 @@ Contract.Requires(var != null);
     ////////////////////////////////////////////////////////////////////////////

 

     protected override void GenSelectStoreFunctions(MapType abstractedType, TypeCtorDecl synonym, out Function/*!*/ select, out Function/*!*/ store) {

-      Contract.Requires(synonym != null);

-      Contract.Requires(abstractedType != null);

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

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

       Contract.Ensures(Contract.ValueAtReturn(out select) != null);

       Contract.Ensures(Contract.ValueAtReturn(out store) != null);

       Type/*!*/ mapTypeSynonym;