Fix contracts so runtime checking can be turned on.

18 files changed, 26 insertions, 68 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) {

diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs
index ef594484..64b6527a 100644
--- a/Source/CodeContractsExtender/cce.cs
+++ b/Source/CodeContractsExtender/cce.cs
@@ -16,7 +16,8 @@ public static class cce {
   //}

   [Pure]

   public static T NonNull<T>(T t) {

-    Contract.Assert(t != null);

+    Contract.Requires(t != null);

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

     return t;

   }

   [Pure]

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7d01bc8f..630f6f14 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1063,12 +1063,7 @@ namespace Microsoft.Boogie {
       }

     }

     private sealed class OldFunctionSymbol : AI.IFunctionSymbol {

-      private static AI.AIType/*!*/ aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type);

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(aitype != null);

-        Contract.Invariant(Sym != null);

-      }

+      private static readonly AI.AIType/*!*/ aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type);

 

       public AI.AIType/*!*/ AIType {

         get {

@@ -1078,7 +1073,7 @@ namespace Microsoft.Boogie {
       }

       private OldFunctionSymbol() {

       }

-      internal static OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol();

+      internal static readonly OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol();

 

       [Pure]

       public override string ToString() {

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 288f5769..96bf358e 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -515,7 +515,6 @@ namespace Microsoft.Boogie {
       Contract.Requires(formalIns != null);

       Contract.Requires(formalOuts != null);

       Contract.Requires(actualIns != null);

-      Contract.Requires(actualOuts != null);

       Contract.Requires(typeCheckingSubject != null);

       Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams)));

       actualTypeParams = new List<Type/*!*/>();

@@ -679,7 +678,6 @@ namespace Microsoft.Boogie {
     public static TypeVariableSeq/*!*/ SortTypeParams(TypeVariableSeq/*!*/ typeParams, TypeSeq/*!*/ argumentTypes, Type resultType) {

       Contract.Requires(typeParams != null);

       Contract.Requires(argumentTypes != null);

-      Contract.Requires(resultType != null);

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

 

       Contract.Ensures(Contract.Result<TypeVariableSeq>().Length == typeParams.Length);

@@ -3586,11 +3584,6 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
     public static readonly TypeParamInstantiation EMPTY =

       new SimpleTypeParamInstantiation(new List<TypeVariable/*!*/>(),

                                         new Dictionary<TypeVariable/*!*/, Type/*!*/>());

-    [ContractInvariantMethod]

-    void EMPTYInvariant() {

-      Contract.Invariant(EMPTY != null);

-    }

-

 

     // return what formal type parameters there are

     public List<TypeVariable/*!*/>/*!*/ FormalTypeParams {

@@ -3626,7 +3619,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
     void ObjectInvariant() {

       Contract.Invariant(Proxy != null);

       Contract.Invariant(ArgumentsResult != null);

-      Contract.Invariant(cce.NonNullElements(Instantiations));

+      Contract.Invariant(Instantiations == null || cce.NonNullElements(Instantiations));

     }

 

 

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 0bc1bce2..2fb29d7a 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -52,7 +52,6 @@ namespace Microsoft.Boogie {
     void ObjectInvariant() {

       Contract.Invariant(_toolname != null);

       Contract.Invariant(_version != null);

-      Contract.Invariant(Clo != null);

       Contract.Invariant(Environment != null);

       Contract.Invariant(FileName != null);

       Contract.Invariant(cce.NonNullElements(Files));

@@ -73,7 +72,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static CommandLineOptions/*!*/ Clo = new CommandLineOptions();  // singleton to access all global data

+    public static readonly CommandLineOptions/*!*/ Clo = new CommandLineOptions();  // singleton to access all global data

 

     public string/*!*/ Environment = "";

     public string/*!*/ FileName = "unknown";

diff --git a/Source/Core/GraphAlgorithms.cs b/Source/Core/GraphAlgorithms.cs
index e901005e..0815e54a 100644
--- a/Source/Core/GraphAlgorithms.cs
+++ b/Source/Core/GraphAlgorithms.cs
@@ -72,10 +72,10 @@ namespace Microsoft.Boogie {
   }

 

   public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> {

-    private readonly IDictionary<Node/*!*/, object/*!*/>/*!*/ graph;

+    private readonly IDictionary<Node/*!*/, object>/*!*/ graph;

     [ContractInvariantMethod]

     void graphInvariantMethod() {

-      Contract.Invariant(cce.NonNullElements(graph));

+      Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null));

       Contract.Invariant(preds != null);

       Contract.Invariant(succs != null);

     }

diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs
index 465b9245..a24343c9 100644
--- a/Source/ParserHelper/ParserHelper.cs
+++ b/Source/ParserHelper/ParserHelper.cs
@@ -47,12 +47,7 @@ namespace Microsoft.Boogie {
     public string/*!*/ _val;  // token value

     public Token next;  // ML 2005-03-11 Tokens are kept in linked list

 

-    public static IToken/*!*/ NoToken = new Token();

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(NoToken != null);

-    }

-

+    public static readonly IToken/*!*/ NoToken = new Token();

 

     public Token() {

       this._val = "anything so that it is nonnull";

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 50eefc49..7f7c4686 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -66,7 +66,7 @@ namespace Microsoft.Boogie.Simplify {
     [StrictReadonly]

     protected readonly ProverOptions options;

     [StrictReadonly]

-    private readonly List<string>/*?*/ commonPrefix;

+    private readonly List<string> commonPrefix;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -75,7 +75,6 @@ namespace Microsoft.Boogie.Simplify {
       Contract.Invariant(openActivityString != null);

       Contract.Invariant(closeActivityString != null);

       Contract.Invariant(options != null);

-      Contract.Invariant(cce.NonNullElements(commonPrefix));

     }

 

 

diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index 4c6fcbb5..7c06af18 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -146,7 +146,6 @@ namespace Microsoft.Boogie.VCExprAST {
     public string this[Object/*!*/ thingie] {

       get {

         Contract.Requires(thingie != null);

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

 

         string res;

         for (int i = LocalNames.Count - 1; i >= 0; --i) {

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 45eeda43..c907bd9f 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -335,14 +335,14 @@ namespace Microsoft.Boogie.VCExprAST {
 

     public static string StoreOpName(VCExprNAry node) {

       Contract.Requires(node != null);

-      Contract.Requires((node.Op is VCExprStoreOp));

+      Contract.Requires((node.Op is VCExprSelectOp) || (node.Op is VCExprStoreOp));

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

       return "Store_" + TypeToString(node[0].Type);

     }

 

     public static string SelectOpName(VCExprNAry node) {

       Contract.Requires(node != null);

-      Contract.Requires((node.Op is VCExprSelectOp));

+      Contract.Requires((node.Op is VCExprSelectOp) || (node.Op is VCExprStoreOp));

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

       return "Select_" + TypeToString(node[0].Type);

     }

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 20c946e5..5f3dbc36 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -633,7 +633,7 @@ namespace Microsoft.Boogie.TypeErasure {
     protected VCExpr GenReverseCastEq(Function castToU, Function castFromU, out VCExprVar var, out List<VCTrigger/*!*/>/*!*/ triggers) {

       Contract.Requires((castFromU != null));

       Contract.Requires((castToU != null));

-      Contract.Requires((cce.NonNullElements(Contract.ValueAtReturn(out triggers))));

+      Contract.Ensures((cce.NonNullElements(Contract.ValueAtReturn(out triggers))));

       Contract.Ensures(Contract.ValueAtReturn(out var) != null);

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

       var = Gen.Variable("x", U);

@@ -1588,7 +1588,7 @@ namespace Microsoft.Boogie.TypeErasure {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(varsInCasts));

-      Contract.Invariant(cce.NonNullElements(varsOutsideCasts));

+      Contract.Invariant(varsOutsideCasts != null && Contract.ForAll(varsOutsideCasts, voc => voc.Key != null));

       Contract.Invariant(AxBuilder != null);

 

     }

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 3e65ec23..c43ee478 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -634,9 +634,10 @@ namespace Microsoft.Boogie.VCExprAST {
       return true;

     }

 

-    public static Dictionary<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {

+    public static Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVariables(VCExpr node) {

       Contract.Requires(node != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));

+      Contract.Ensures(Contract.Result<Dictionary<VCExprVar, object>>() != null);

+      Contract.Ensures(Contract.ForAll(Contract.Result<Dictionary<VCExprVar, object>>(), ftv => ftv.Key != null));

       FreeVariableCollector collector = new FreeVariableCollector();

       collector.Traverse(node, true);

       return collector.FreeTermVars;

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 5323bb03..20b17e6b 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -507,8 +507,8 @@ namespace VC {
     public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);

-      Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

 

+      Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

       Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       Helpers.ExtraTraceInformation("Starting implementation verification");

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index c57863a3..c418f828 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1496,7 +1496,6 @@ namespace VC
             Contract.Requires(vState.calls != null);

             Contract.Requires(vState.checker != null);

             Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

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

 

             var checker = vState.checker.underlyingChecker;

             var calls = vState.calls;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 87f78a96..0215784b 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -73,7 +73,7 @@ namespace VC {
         Contract.Invariant(controlFlowVariable != null);

         Contract.Invariant(assertExpr != null);

         Contract.Invariant(cce.NonNullElements(interfaceVars));

-        Contract.Invariant(cce.NonNullElements(incarnationOriginMap));

+        Contract.Invariant(incarnationOriginMap == null || cce.NonNullElements(incarnationOriginMap));

       }

 

       public Implementation impl;

@@ -145,7 +145,7 @@ namespace VC {
     }

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(cce.NonNullElements(implName2LazyInliningInfo));

+      Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullElements(implName2LazyInliningInfo));

     }

 

     private Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

@@ -2678,7 +2678,6 @@ namespace VC {
       Contract.Requires(b != null);

       Contract.Requires(traceNodes != null);

       Contract.Requires(trace != null);

-      Contract.Requires(errModel != null);

       Contract.Requires(cce.NonNullElements(incarnationOriginMap));

       Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));

       Contract.Requires(context != null);

@@ -3525,7 +3524,6 @@ namespace VC {
                         Hashtable/*<int, Absy!>*/ label2absy,

                         ProverContext proverCtxt) {

       Contract.Requires(startBlock != null);

-      Contract.Requires(controlFlowVariable != null);

       Contract.Requires(label2absy != null);

       Contract.Requires(proverCtxt != null);

 

@@ -3545,7 +3543,6 @@ namespace VC {
                         ProverContext proverCtxt)

     {

       Contract.Requires(block != null);

-      Contract.Requires(controlFlowVariable != null);

       Contract.Requires(label2absy != null);

       Contract.Requires(blockVariables!= null);

       Contract.Requires(cce.NonNullElements(bindings));

@@ -3833,7 +3830,6 @@ namespace VC {
         Microsoft.Boogie.VCExpressionGenerator gen) {

       Contract.Requires(b != null);

       Contract.Requires(BlkCorrect != null);

-      Contract.Requires(BlkReached != null);

       Contract.Requires(totalOrder != null);

       Contract.Requires(g != null);

       Contract.Requires(context != null);