Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on.

1 files changed, 38 insertions, 37 deletions

diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs
index 7979f061..34564cac 100644
--- a/Source/AbsInt/ExprFactories.cs
+++ b/Source/AbsInt/ExprFactories.cs
@@ -27,42 +27,42 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public AI.IFunApp Not(AI.IExpr p) {

-      Contract.Requires(p != null);

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

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

 

       return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p));

     }

 

     public AI.IFunApp And(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

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

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

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

 

       return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

     }

 

     public AI.IFunApp Or(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

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

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

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

       return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q));

     }

 

     public AI.IFunApp Implies(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

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

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

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

       return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q));

     }

 

     public AI.IFunApp Exists(AI.IFunction p) {

-      Contract.Requires(p != null);

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

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

 

       return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

     }

     public AI.IFunApp Exists(AI.AIType paramType, AI.FunctionBody bodygen) {

-      Contract.Requires(bodygen != null);

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

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

 

       // generate a fresh new variable

@@ -74,13 +74,13 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public AI.IFunApp Forall(AI.IFunction p) {

-      Contract.Requires(p != null);

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

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

 

       return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

     }

     public AI.IFunApp Forall(AI.AIType paramType, AI.FunctionBody bodygen) {

-      Contract.Requires(bodygen != null);

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

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

 

       // generate a fresh new variable

@@ -116,15 +116,15 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 

   public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory {

     public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

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

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

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

 

       return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

     public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

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

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

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

       return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

@@ -132,15 +132,15 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 

   public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory {

     public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

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

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

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

       return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

 

     public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

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

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

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

       return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

     }

@@ -163,14 +163,14 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 

   public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory {

     public AI.IFunApp AtMost(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

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

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

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

       return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1));

     }

     public AI.IFunApp Add(AI.IExpr e0, AI.IExpr e1) {

-      Contract.Requires(e0 != null);

-      Contract.Requires(e1 != null);

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

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

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

       return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1));

     }

@@ -208,8 +208,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       }

     }

     public AI.IFunApp And(AI.IExpr p, AI.IExpr q) {

-      Contract.Requires(p != null);

-      Contract.Requires(q != null);

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

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

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

 

       return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

@@ -232,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// </summary>

     [Pure]

     public bool IsTypeConstant(AI.IExpr t) {

-      Contract.Requires(t != null);

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

       Contract.Ensures(Contract.Result<bool>() == (t is Constant));

       return t is Constant;

     }

@@ -242,8 +242,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// </summary>

     [Pure]

     public bool IsTypeEqual(AI.IExpr t0, AI.IExpr t1) {

-      Contract.Requires(t0 != null);

-      Contract.Requires(t1 != null);

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

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

       Constant c0 = t0 as Constant;

       Constant c1 = t1 as Constant;

       return c0 != null && c1 != null && c0 == c1;

@@ -254,8 +254,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// </summary>

     [Pure]

     public bool IsSubType(AI.IExpr t0, AI.IExpr t1) {

-      Contract.Requires(t0 != null);

-      Contract.Requires(t1 != null);

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

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

 

       Contract.Assert(false);  // BUGBUG: TODO

       throw new cce.UnreachableException();

@@ -266,8 +266,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     /// that "t0" and "t1" both represent types.

     /// </summary>

     public AI.IExpr JoinTypes(AI.IExpr t0, AI.IExpr t1) {

-      Contract.Requires(t0 != null);

-      Contract.Requires(t1 != null);

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

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

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

 

 

@@ -279,8 +279,8 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       //PM: We need this assume because Boogie does not yet allow us to use the

       //PM: inherited precondition "requires IsTypeConstant(type)".

       //PM: Note that that precondition is currently commented out.

-      Contract.Requires(e != null);

-      Contract.Requires(type != null);

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

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

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

 

       Contract.Assume(type is Constant);

@@ -295,12 +295,13 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     }

 

     public AI.IFunApp IsA(AI.IExpr e, AI.IExpr type) {

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

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

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

       //PM: We need this assume because Boogie does not yet allow us to use the

       //PM: inherited precondition "requires IsTypeConstant(type)".

       //PM: Note that that precondition is currently commented out.

-      Contract.Requires(e != null);

-      Contract.Requires(type != null);

-      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      

 

       Contract.Assume(type is Constant);

       Contract.Assert(false);