Boogie: Removed some errors with code contracts (commenting out doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).

1 files changed, 88 insertions, 87 deletions

diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs
index 84525a15..78bd61a0 100644
--- a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs
+++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs
@@ -163,100 +163,101 @@ namespace Microsoft.AbstractInterpretationFramework {
     }

 

     public override bool IsTop(Element/*!*/ element) {

-      Contract.Requires(element != null);

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

       Elt e = (Elt)element;

       return e.what == What.Bounds && e.ty == null && e.manyBounds == null;

     }

 

     public override bool IsBottom(Element/*!*/ element) {

-      Contract.Requires(element != null);

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

       Elt e = (Elt)element;

       return e.what == What.Bottom;

     }

 

-    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second){

-Contract.Requires(second != null);

-Contract.Requires(first != null);

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

-            Elt a = (Elt)first;

-            Elt b = (Elt)second;

-            Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);

-            if (a.what == What.Exact && b.what == What.Exact) {

-                Contract.Assert(a.ty != null && b.ty != null);

-                if (factory.IsTypeEqual(a.ty, b.ty)) {

-                    return a;

-                } else {

-                    return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));

-                }

-            }

+    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {

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

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

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

+      Elt a = (Elt)first;

+      Elt b = (Elt)second;

+      Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);

+      if (a.what == What.Exact && b.what == What.Exact) {

+        Contract.Assert(a.ty != null && b.ty != null);

+        if (factory.IsTypeEqual(a.ty, b.ty)) {

+          return a;

+        } else {

+          return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));

+        }

+      }

 

-            // The result is going to be a Bounds, since at least one of the operands is a Bounds.

-            Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount);  // a preconditions is that neither operand is Top

-            int n = a.BoundsCount + b.BoundsCount;

-

-            // Special case:  a and b each has exactly one bound

-            if (n == 2) {

-                Contract.Assert(a.ty != null && b.ty != null);

-                IExpr join = factory.JoinTypes(a.ty, b.ty);

-              Contract.Assert(join != null);

-                if (join == a.ty && a.what == What.Bounds) {

-                    return a;

-                } else if (join == b.ty && b.what == What.Bounds) {

-                    return b;

-                } else {

-                    return new Elt(What.Bounds, join);

-                }

-            }

+      // The result is going to be a Bounds, since at least one of the operands is a Bounds.

+      Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount);  // a preconditions is that neither operand is Top

+      int n = a.BoundsCount + b.BoundsCount;

 

-            // General case

-            ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);  // final size

-            ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n);  // a guess at the size, but could be as big as size(a)*size(b)

-            if (a.ty != null) {

-                allBounds.Add(a.ty);

-            } else {

-                allBounds.AddRange(cce.NonNull(a.manyBounds));

-            }

-            int bStart = allBounds.Count;

-            if (b.ty != null) {

-                allBounds.Add(b.ty);

+      // Special case:  a and b each has exactly one bound

+      if (n == 2) {

+        Contract.Assert(a.ty != null && b.ty != null);

+        IExpr join = factory.JoinTypes(a.ty, b.ty);

+        Contract.Assert(join != null);

+        if (join == a.ty && a.what == What.Bounds) {

+          return a;

+        } else if (join == b.ty && b.what == What.Bounds) {

+          return b;

+        } else {

+          return new Elt(What.Bounds, join);

+        }

+      }

+

+      // General case

+      ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);  // final size

+      ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n);  // a guess at the size, but could be as big as size(a)*size(b)

+      if (a.ty != null) {

+        allBounds.Add(a.ty);

+      } else {

+        allBounds.AddRange(cce.NonNull(a.manyBounds));

+      }

+      int bStart = allBounds.Count;

+      if (b.ty != null) {

+        allBounds.Add(b.ty);

+      } else {

+        allBounds.AddRange(cce.NonNull(b.manyBounds));

+      }

+      // compute the join of each pair, putting non-redundant joins into "result"

+      for (int i = 0; i < bStart; i++) {

+        IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);

+        for (int j = bStart; j < allBounds.Count; j++) {

+          IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);

+

+          IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);

+          Contract.Assert(join != null);

+

+          int k = 0;

+          while (k < result.Count) {

+            IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]);

+            if (factory.IsSubType(join, r)) {

+              // "join" is more restrictive than a bound already placed in "result",

+              // so toss out "join" and compute the join of the next pair

+              goto NEXT_PAIR;

+            } else if (factory.IsSubType(r, join)) {

+              // "join" is less restrictive than a bound already placed in "result",

+              // so toss out that old bound

+              result.RemoveAt(k);

             } else {

-                allBounds.AddRange(cce.NonNull(b.manyBounds));

+              k++;

             }

-            // compute the join of each pair, putting non-redundant joins into "result"

-            for (int i = 0; i < bStart; i++) {

-                IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);

-                for (int j = bStart; j < allBounds.Count; j++) {

-                    IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);

-                    

-                    IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);

-                  Contract.Assert(join != null);

-

-                    int k = 0;

-                    while (k < result.Count) {

-                      IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]);

-                        if (factory.IsSubType(join, r)) {

-                            // "join" is more restrictive than a bound already placed in "result",

-                            // so toss out "join" and compute the join of the next pair

-                            goto NEXT_PAIR;

-                        } else if (factory.IsSubType(r, join)) {

-                            // "join" is less restrictive than a bound already placed in "result",

-                            // so toss out that old bound

-                            result.RemoveAt(k);

-                        } else {

-                            k++;

-                        }

-                    }

-                    result.Add(join);

-                    NEXT_PAIR: {}

-                }

-            }

-            return new Elt(result, result.Count);

+          }

+          result.Add(join);

+        NEXT_PAIR: {

+          }

         }

+      }

+      return new Elt(result, result.Count);

+    }

 

 

     public override Element/*!*/ NontrivialMeet(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;

@@ -359,16 +360,16 @@ Contract.Ensures(Contract.Result<Element>() != null);
     }

 

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

       return Join(first, second);

     }

 

     protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that

     {

-      Contract.Requires(first != null);

-      Contract.Requires(second != null);

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

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

       Elt/*!*/ a = (Elt/*!*/)cce.NonNull(first);

       Elt/*!*/ b = (Elt/*!*/)cce.NonNull(second);

       Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);

@@ -403,8 +404,8 @@ Contract.Ensures(Contract.Result<Element>() != null);
     }

 

     public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {

-      Contract.Requires(element != null);

-      Contract.Requires(var != null);

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

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

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

       Elt e = (Elt)element;

       switch (e.what) {

@@ -433,14 +434,14 @@ Contract.Ensures(Contract.Result<Element>() != null);
     }

 

     public override IExpr GetFoldExpr(Element/*!*/ e) {

-      Contract.Requires(e != null);

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

       // cannot fold into an expression that can be substituted for the variable

       return null;

     }

 

     public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {

-      Contract.Requires(args != null);

-      Contract.Requires(f != null);

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

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

       bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);

       if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {

         Contract.Assert(args.Count == 2);

@@ -470,7 +471,7 @@ Contract.Ensures(Contract.Result<Element>() != null);
     }

 

     public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {

-      Contract.Requires(e != null);

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

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

       IFunApp nary = e as IFunApp;

       if (nary != null) {