Fixed errors in the use of Code Contracts

7 files changed, 25 insertions, 30 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0e095c44..0dbcaaba 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -39,6 +39,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       public readonly BigInteger? Lo;

       public readonly BigInteger? Hi;

       public Node Next;  // always sorted according to StrictlyBefore; readonly after full initialization

+      [Pure]

       public static bool StrictlyBefore(Variable a, Variable b) {

         Contract.Assert(a.UniqueId != b.UniqueId || a == b);

         return a.UniqueId < b.UniqueId;

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index f0e2e7ed..b220b373 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -783,7 +783,7 @@ namespace Microsoft.Boogie {
 

     public static Graph<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) {

       Contract.Requires(impl != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().TopologicalSort()));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().Nodes));

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

 

       Graph<Block/*!*/> g = new Graph<Block/*!*/>();

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 06d72ee9..e2bbcdf5 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -271,6 +271,7 @@ namespace Microsoft.Boogie {
       current.Next = other;

     }

     // Look for {:name string} in list of attributes.

+    [Pure]

     public static string FindStringAttribute(QKeyValue kv, string name) {

       Contract.Requires(name != null);

       for (; kv != null; kv = kv.Next) {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index b89219a9..bdfefb04 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -132,26 +132,23 @@ namespace Microsoft.Boogie {
           }

       }

 

-      if (false /*CommandLineOptions.Clo.Trace*/)      {

-

-          Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count);

-          foreach (Procedure/*!*/ x in modSets.Keys)

-          {

-              Contract.Assert(x != null);

-              Console.Write("{0} : ", x.Name);

-              bool first = true;

-              foreach (Variable/*!*/ y in modSets[x])

-              {

-                  Contract.Assert(y != null);

-                  if (first)

-                      first = false;

-                  else

-                      Console.Write(", ");

-                  Console.Write("{0}", y.Name);

-              }

-              Console.WriteLine("");

-          }

+#if DEBUG_PRINT

+      Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count);

+      foreach (Procedure/*!*/ x in modSets.Keys) {

+        Contract.Assert(x != null);

+        Console.Write("{0} : ", x.Name);

+        bool first = true;

+        foreach (Variable/*!*/ y in modSets[x]) {

+          Contract.Assert(y != null);

+          if (first)

+            first = false;

+          else

+            Console.Write(", ");

+          Console.Write("{0}", y.Name);

+        }

+        Console.WriteLine("");

       }

+#endif

     }

 

     public override Implementation VisitImplementation(Implementation node) {

@@ -722,7 +719,7 @@ namespace Microsoft.Boogie {
     public Implementation/*!*/ impl;

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

+      Contract.Invariant(cce.NonNullElements(graph.Nodes));

       Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled));

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

       Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges));

@@ -892,7 +889,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(cce.NonNullDictionaryAndValues(name2Proc));

       Contract.Invariant(cce.NonNullDictionaryAndValues(callers) &&

         Contract.ForAll(callers.Values, v => cce.NonNullElements(v)));

-      Contract.Invariant(cce.NonNullElements(callGraph.TopologicalSort()));

+      Contract.Invariant(cce.NonNullElements(callGraph.Nodes));

       Contract.Invariant(procPriority != null);

       Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtEntry));

       Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtExit) &&

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index a11c93ec..650bb146 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -370,9 +370,9 @@ namespace Microsoft.Boogie {
     }

     public override YieldCmd VisitYieldCmd(YieldCmd node)

     {

-        //Contract.Requires(node != null);

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

-        return base.VisitYieldCmd((YieldCmd)node.Clone());

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

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

+      return base.VisitYieldCmd((YieldCmd)node.Clone());

     }

   }

 

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index e883d0bd..b05a2e5f 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -248,8 +248,6 @@ namespace Microsoft.Boogie.Houdini {
 

   public class InlineRequiresVisitor : StandardVisitor {

     public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {

-      Contract.Requires(cmdSeq != null);

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

       List<Cmd> newCmdSeq = new List<Cmd>();

       for (int i = 0, n = cmdSeq.Count; i < n; i++) {

         Cmd cmd = cmdSeq[i];

@@ -289,8 +287,6 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {

-      Contract.Requires(node != null);

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

       node.Requires = base.VisitRequires(node.Requires);

       node.Expr = this.VisitExpr(node.Expr);

       return node;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index b0be1072..49ae68e3 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2306,7 +2306,7 @@ namespace VC {
       Contract.Requires(taskID == -1);

 

       int inductionK = CommandLineOptions.Clo.KInductionDepth;

-      Contract.Requires(inductionK >= 0);

+      Contract.Assume(inductionK >= 0);

 

       bool contRuleApplication = true;

       while (contRuleApplication) {