From f09bf83d24438d712021ada6fab252b0f7f11986 Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Fri, 27 Aug 2010 21:52:03 +0000
Subject: Boogie: Commented out all occurences of repeated inherited contracts
 - makes fewer error messages when compiling with runtime checking on.

---
 Source/AbsInt/ExprFactories.cs | 75 +++++++++++++++++++++---------------------
 1 file changed, 38 insertions(+), 37 deletions(-)

(limited to 'Source/AbsInt')

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);
-- 
cgit v1.2.3