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

4 files changed, 14 insertions, 121 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;

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index d577c048..fb68eefd 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -110,7 +110,6 @@
     </Reference>

   </ItemGroup>

   <ItemGroup>

-    <Compile Include="cce.cs" />

     <Compile Include="DafnyDriver.cs" />

     <Compile Include="..\version.cs" />

   </ItemGroup>

diff --git a/Source/DafnyDriver/cce.cs b/Source/DafnyDriver/cce.cs
deleted file mode 100644
index 34749b5f..00000000
--- a/Source/DafnyDriver/cce.cs
+++ /dev/null
@@ -1,104 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Diagnostics.Contracts;

-using System.Text;

-using Microsoft.Boogie;

-

-  /// <summary>

-    /// A class containing static methods to extend the functionality of Code Contracts

-    /// </summary>

-

-public static class cce {

-  [Pure]

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

-    Contract.Assert(t != null);

-    return t;

-  }

-  [Pure]

-  public static bool NonNullElements<T>(IEnumerable<T> collection) {

-    return collection != null && Contract.ForAll(collection, c => c != null);

-  }

-  [Pure]

-  public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {

-    return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values);

-  }

-  [Pure]

-  public static bool NonNullElements(VariableSeq collection) {

-    return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

-  }

-  [Pure]

-  public static void BeginExpose(object o) {

-  }

-  [Pure]

-  public static void EndExpose() {

-  }

-  [Pure]

-  public static bool IsPeerConsistent(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsConsistent(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsExposable(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsExposed(object o) {

-    return true;

-  }

-  public static class Owner {

-    [Pure]

-    public static bool Same(object o, object p) {

-      return true;

-    }

-    [Pure]

-    public static void AssignSame(object o, object p) {

-    }

-    [Pure]

-    public static object ElementProxy(object o) {

-      return o;

-    }

-    [Pure]

-    public static bool None(object o) {

-      return true;

-    }

-  }

-  [Pure]

-  public static void LoopInvariant(bool p) {

-    Contract.Assert(p);

-  }

-

-  public class UnreachableException : Exception {

-    public UnreachableException() {

-    }

-  }

-}

-

-public class PeerAttribute : System.Attribute {

-}

-public class RepAttribute : System.Attribute {

-}

-public class CapturedAttribute : System.Attribute {

-}

-public class NotDelayedAttribute : System.Attribute {

-}

-public class NoDefaultContractAttribute : System.Attribute {

-}

-public class VerifyAttribute : System.Attribute {

-  public VerifyAttribute(bool b) {

-

-  }

-}

-public class StrictReadonlyAttribute : System.Attribute {

- }

-public class AdditiveAttribute : System.Attribute {

-}

-public class ReadsAttribute : System.Attribute {

-  public enum Reads {

-    Nothing,

-  };

-  public ReadsAttribute(object o) {

-  }

-}
\ No newline at end of file