Fix contracts so runtime checking can be turned on.

4 files changed, 6 insertions, 25 deletions

diff --git a/Source/AIFramework/CommonFunctionSymbols.cs b/Source/AIFramework/CommonFunctionSymbols.cs
index 7dbfdd03..d8e4497f 100644
--- a/Source/AIFramework/CommonFunctionSymbols.cs
+++ b/Source/AIFramework/CommonFunctionSymbols.cs
@@ -220,15 +220,6 @@ Contract.Ensures(Contract.Result<FunctionType>() != null);
         }

 

         [Once] private static AIType/*!*/ binreltype;

-      [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(binreltype != null);

-        Contract.Invariant(_eq != null);

-        Contract.Invariant(_neq != null);

-        Contract.Invariant(_subtype != null);

-        Contract.Invariant(_typeof != null);

-}

 

         private static AIType/*!*/ BinrelType {

           get {Contract.Ensures(Contract.Result<AIType>() != null);

@@ -462,7 +453,7 @@ Contract.Requires(f != null);
         private static readonly AIType/*!*/ heaptype = new Heap();

         public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return heaptype; } }

 

-        // the types in the following, select1, select2, are hard-coded;
+        // the types in the following, select1, select2, are hard-coded;

         // these types may not always be appropriate

         private static readonly FunctionSymbol/*!*/ _select1 = new FunctionSymbol("sel1",

             // Heap x FieldName -> Prop

@@ -476,7 +467,7 @@ Contract.Requires(f != null);
         );

         public static FunctionSymbol/*!*/ Select2 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _select2; } }

 

-        // the types in the following, store1, store2, are hard-coded;
+        // the types in the following, store1, store2, are hard-coded;

         // these types may not always be appropriate

         private static readonly FunctionSymbol/*!*/ _update1 = new FunctionSymbol("upd1",

             // Heap x FieldName x Value -> Heap

@@ -626,11 +617,6 @@ Contract.Requires(f != null);
     public sealed class Prop : AIType

     {

         private static readonly AIType/*!*/ proptype = new Prop();

-      [ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(proptype != null);

-}

 

         public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return proptype; } }

 

diff --git a/Source/AIFramework/Functional.cs b/Source/AIFramework/Functional.cs
index 531ce94f..3b8237bf 100644
--- a/Source/AIFramework/Functional.cs
+++ b/Source/AIFramework/Functional.cs
@@ -111,7 +111,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections {
 

     object IFunctionalMap.this[object key] {

       get {

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

+        Contract.Requires(key != null);

         throw new System.NotImplementedException();

       }

     }

diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
index b6ce193a..299d49cf 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
+++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
@@ -1273,7 +1273,7 @@ Contract.Requires(oldName != null);
     static void SimplifyFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, bool vertices, ArrayList/*!*/ /*LinearConstraint*/ constraints, out SimplificationStatus[]/*!*/ status) {

       Contract.Requires(ff != null);

       Contract.Requires(constraints != null);

-      Contract.Requires(Contract.ValueAtReturn(out status) != null);

+      Contract.Ensures(Contract.ValueAtReturn(out status) != null);

       status = new SimplificationStatus[ff.Count];

       bool[,] sat = new bool[ff.Count, constraints.Count];

       for (int i = 0; i < ff.Count; i++) {

diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs
index b3c702d7..b60d318b 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.cs
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs
@@ -64,13 +64,8 @@ namespace Microsoft.AbstractInterpretationFramework {
         return s + "]";

       }

 

-      public static Elt/*!*/ Top = new Elt(true);

-      public static Elt/*!*/ Bottom = new Elt(false);

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(Top != null);

-        Contract.Invariant(Bottom != null);

-      }

+      public static readonly Elt/*!*/ Top = new Elt(true);

+      public static readonly Elt/*!*/ Bottom = new Elt(false);

 

 

       public Elt(IFunctionalMap constraints) {