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/AIFramework/Lattice.cs                        |  2 +-
 Source/AIFramework/VariableMap/VariableMapLattice.cs | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'Source/AIFramework')

diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs
index 78f87421..8d7f6c45 100644
--- a/Source/AIFramework/Lattice.cs
+++ b/Source/AIFramework/Lattice.cs
@@ -792,7 +792,7 @@ namespace Microsoft.AbstractInterpretationFramework {
 
     public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
       //Contract.Requires(args != null);
-      Contract.Requires(f != null);
+      //Contract.Requires(f != null);
       understandsCount++;
       return lattice.Understands(f, args);
     }
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs
index 169156b0..b3c702d7 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.cs
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs
@@ -329,7 +329,7 @@ namespace Microsoft.AbstractInterpretationFramework {
     }
 
     public override string/*!*/ ToString(Element/*!*/ element) {
-      Contract.Requires(element != null);
+      //Contract.Requires(element != null);
       Contract.Ensures(Contract.Result<string>() != null);
       Elt e = (Elt)element;
 
@@ -416,8 +416,8 @@ namespace Microsoft.AbstractInterpretationFramework {
     /// Perform the pointwise widening of the elements in the map
     /// </summary>
     public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
-      Contract.Requires((second != null));
-      Contract.Requires((first != null));
+      //Contract.Requires((second != null));
+      //Contract.Requires((first != null));
       Contract.Ensures(Contract.Result<Element>() != null);
       Elt a = (Elt)first;
       Elt b = (Elt)second;
@@ -568,7 +568,7 @@ namespace Microsoft.AbstractInterpretationFramework {
     }
 
     public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
-      Contract.Requires(element != null);
+      //Contract.Requires(element != null);
       Contract.Ensures(Contract.Result<IExpr>() != null);
       if (IsTop(element)) {
         return propExprFactory.True;
@@ -765,8 +765,8 @@ namespace Microsoft.AbstractInterpretationFramework {
 
 
     public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
-      Contract.Requires(args != null);
-      Contract.Requires(f != null);
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
       return f.Equals(Prop.And) ||
              f.Equals(Value.Eq) ||
              microLattice.Understands(f, args);
-- 
cgit v1.2.3