Dafny: Fixed some build issues with duplicated and malformed Code Contracts.

2 files changed, 14 insertions, 16 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 1e355f63..012d402a 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -581,7 +581,7 @@ namespace Microsoft.Dafny {
         if (t.ArrayDimensions != null) {

           string s = "[";

           foreach (Expression dim in t.ArrayDimensions) {

-            Contract.Requires(dim != null);

+            Contract.Assume(dim != null);

             wr.Write(s);

             PrintExpression(dim);

             s = ", ";

diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index 66541236..ba3e2084 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -12,12 +12,11 @@ namespace Microsoft.Dafny {
       public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();

       public List<Vertex/*!*/> SccMembers;  // non-null only for the representative of the SCC

       [ContractInvariantMethod]

-void ObjectInvariant() 

-{

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

-        if(SccMembers!=null)

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

-}

+      void ObjectInvariant() 

+      {

+        Contract.Invariant(cce.NonNullElements(Successors));

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

+      }

 

       public Vertex SccRepresentative;  // null if not computed

       

@@ -40,15 +39,14 @@ void ObjectInvariant()
     }

 

 

-[ContractInvariantMethod]

-void ObjectInvariant() 

-{

-    Contract.Invariant(vertices!=null);

-  Contract.Invariant(cce.NonNullElements(vertices.Values));

-  if(topologicallySortedRepresentatives!=null)

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

-  Contract.Invariant(!sccComputed || topologicallySortedRepresentatives != null);

-}

+    [ContractInvariantMethod]

+    void ObjectInvariant() 

+    {

+      Contract.Invariant(vertices!=null);

+      Contract.Invariant(cce.NonNullElements(vertices.Values));

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

+      Contract.Invariant(!sccComputed || topologicallySortedRepresentatives != null);

+    }

 

     Dictionary<Node, Vertex/*!*/>/*!*/ vertices = new Dictionary<Node, Vertex/*!*/>();

     bool sccComputed = false;