Boogie: Graph port 3/3: Committing changed references; also, adding back cce files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.

18 files changed, 916 insertions, 64 deletions

diff --git a/Source/AIFramework/AIFramework.csproj b/Source/AIFramework/AIFramework.csproj
index bddd07f2..224be513 100644
--- a/Source/AIFramework/AIFramework.csproj
+++ b/Source/AIFramework/AIFramework.csproj
@@ -70,7 +70,9 @@
     <Reference Include="System" />

   </ItemGroup>

   <ItemGroup>

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

+    <Compile Include="cce.cs">

+      <SubType>Code</SubType>

+    </Compile>

     <Compile Include="CommonFunctionSymbols.cs" />

     <Compile Include="Expr.cs" />

     <Compile Include="Functional.cs" />

diff --git a/Source/AIFramework/cce.cs b/Source/AIFramework/cce.cs
index 76deba32..ef594484 100644
--- a/Source/AIFramework/cce.cs
+++ b/Source/AIFramework/cce.cs
@@ -3,7 +3,7 @@ using SA=System.Attribute;
 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Text;

-using Microsoft.Boogie;

+//using Microsoft.Boogie;

 

 /// <summary>

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

@@ -131,9 +131,9 @@ public static class cce {
   //  return toRet;

   //}

 

-  internal static bool NonNullElements(Set set) {

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

-  }

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

 }

 

 public class PeerAttribute : SA {

diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index c5601053..62d90dff 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -81,6 +81,7 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="AbstractInterpretation.cs" />

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

     <Compile Include="ExprFactories.cs" />

     <Compile Include="LoopInvariantsOnDemand.cs" />

     <Compile Include="Traverse.cs" />

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 9020382d..8ac6b180 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -5,8 +5,6 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758
 EndProject

 Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Basetypes", "Basetypes\Basetypes.sscproj", "{0C692837-77EC-415F-BF04-395E3ED06E9A}"

 EndProject

-Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Graph", "Graph\Graph.sscproj", "{4C28FB90-630E-4B55-A937-11A011B79765}"

-EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"

 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabelle\Isabelle.csproj", "{435D5BD0-6F62-49F8-BB24-33E2257519AD}"

@@ -29,6 +27,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Z3api", "Provers\Z3api\Z3ap
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AIFramework", "AIFramework\AIFramework.csproj", "{39B0658D-C955-41C5-9A43-48C97A1EF5FD}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj", "{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|.NET = Debug|.NET

@@ -49,16 +49,6 @@ Global
 		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Any CPU.ActiveCfg = Release|.NET

 		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Mixed Platforms.ActiveCfg = Release|.NET

 		{0C692837-77EC-415F-BF04-395E3ED06E9A}.Release|Mixed Platforms.Build.0 = Release|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|.NET.ActiveCfg = Debug|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|.NET.Build.0 = Debug|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Any CPU.ActiveCfg = Debug|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Debug|Mixed Platforms.Build.0 = Debug|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|.NET.ActiveCfg = Release|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|.NET.Build.0 = Release|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|Any CPU.ActiveCfg = Release|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|Mixed Platforms.ActiveCfg = Release|.NET

-		{4C28FB90-630E-4B55-A937-11A011B79765}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.Build.0 = Debug|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

@@ -175,6 +165,16 @@ Global
 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Any CPU.Build.0 = Release|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{39B0658D-C955-41C5-9A43-48C97A1EF5FD}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|.NET.ActiveCfg = Release|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Any CPU.Build.0 = Release|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Release|Mixed Platforms.Build.0 = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index a31019db..5b08ba0d 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -87,6 +87,7 @@
   <ItemGroup>

     <Compile Include="BoogieDriver.cs" />

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

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

   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\AbsInt\AbsInt.csproj">

@@ -105,8 +106,8 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Graph\Graph.sscproj">

-      <Project>{4C28FB90-630E-4B55-A937-11A011B79765}</Project>

+    <ProjectReference Include="..\Graph\Graph.csproj">

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\Provers\Isabelle\Isabelle.csproj">

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 54bc2cab..212e8208 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -92,6 +92,7 @@
     <Compile Include="AbsyExpr.cs" />

     <Compile Include="AbsyQuant.cs" />

     <Compile Include="AbsyType.cs" />

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

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="DeadVarElim.cs" />

     <Compile Include="Duplicator.cs" />

@@ -121,8 +122,8 @@
       <Project>{0C692837-77EC-415F-BF04-395E3ED06E9A}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Graph\Graph.sscproj">

-      <Project>{4C28FB90-630E-4B55-A937-11A011B79765}</Project>

+    <ProjectReference Include="..\Graph\Graph.csproj">

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/Core/cce.cs b/Source/Core/cce.cs
index 7aade95e..ef594484 100644
--- a/Source/Core/cce.cs
+++ b/Source/Core/cce.cs
@@ -3,7 +3,7 @@ using SA=System.Attribute;
 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Text;

-using Microsoft.Boogie;

+//using Microsoft.Boogie;

 

 /// <summary>

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

@@ -27,10 +27,10 @@ public static class cce {
   public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {

     return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));

   }

-  [Pure]

-  public static bool NonNullElements(VariableSeq collection) {

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

-  }

+  //[Pure]

+  //public static bool NonNullElements(VariableSeq collection) {

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

+  //}

   /// <summary>

   /// For possibly-null lists of non-null elements

   /// </summary>

@@ -123,13 +123,17 @@ public static class cce {
   //public static bool IsValid(Microsoft.Dafny.Expression expression) {

   //  return true;

   //}

-  public static List<T> toList<T>(PureCollections.Sequence s) {

-    List<T> toRet = new List<T>();

-    foreach (T t in s.elems)

-      if(t!=null)

-      toRet.Add(t);

-    return toRet;

-  }

+  //public static List<T> toList<T>(PureCollections.Sequence s) {

+  //  List<T> toRet = new List<T>();

+  //  foreach (T t in s.elems)

+  //    if(t!=null)

+  //    toRet.Add(t);

+  //  return toRet;

+  //}

+

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

 }

 

 public class PeerAttribute : SA {

@@ -184,4 +188,6 @@ public class SpecPublicAttribute : SA {
 public class ElementsPeerAttribute : SA {

 }

 public class ResultNotNewlyAllocatedAttribute : SA {

+}

+public class OnceAttribute : SA {

 }
\ No newline at end of file
diff --git a/Source/Provers/Isabelle/Isabelle.csproj b/Source/Provers/Isabelle/Isabelle.csproj
index bcf367b7..e48b0fa7 100644
--- a/Source/Provers/Isabelle/Isabelle.csproj
+++ b/Source/Provers/Isabelle/Isabelle.csproj
@@ -69,6 +69,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Prover.cs" />

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

   </ItemGroup>

diff --git a/Source/Provers/Isabelle/cce.cs b/Source/Provers/Isabelle/cce.cs
new file mode 100644
index 00000000..ef594484
--- /dev/null
+++ b/Source/Provers/Isabelle/cce.cs
@@ -0,0 +1,193 @@
+using System;

+using SA=System.Attribute;

+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 bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

+  //}

+  [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 && Contract.ForAll(collection, pair => NonNullElements(pair));

+  }

+  //[Pure]

+  //public static bool NonNullElements(VariableSeq collection) {

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

+  //}

+  /// <summary>

+  /// For possibly-null lists of non-null elements

+  /// </summary>

+  /// <typeparam name="T"></typeparam>

+  /// <param name="collection"></param>

+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>

+  /// <returns></returns>

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {

+    return (nullability && collection == null) || cce.NonNullElements(collection);

+    //Should be the same as:

+    /*if(nullability&&collection==null)

+     * return true;

+     * return cce.NonNullElements(collection)

+     */

+

+  }

+  [Pure]

+  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {

+    return kvp.Key != null && kvp.Value != null;

+  }

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

+    return iEnumerator != null;

+  }

+  //[Pure]

+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

+  //  return cce.NonNullElements(graph.TopologicalSort());

+  //}

+  [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;

+  }

+  [Pure]

+  public static bool IsNew(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 bool Different(object o, object p) {

+      return true;

+    }

+    [Pure]

+    public static bool New(object o) {

+      return true;

+    }

+  }

+  [Pure]

+  public static void LoopInvariant(bool p) {

+    Contract.Assert(p);

+  }

+  public class UnreachableException : Exception {

+    public UnreachableException() {

+    }

+  }

+  //[Pure]

+  //public static bool IsValid(Microsoft.Dafny.Expression expression) {

+  //  return true;

+  //}

+  //public static List<T> toList<T>(PureCollections.Sequence s) {

+  //  List<T> toRet = new List<T>();

+  //  foreach (T t in s.elems)

+  //    if(t!=null)

+  //    toRet.Add(t);

+  //  return toRet;

+  //}

+

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

+}

+

+public class PeerAttribute : SA {

+}

+public class RepAttribute : SA {

+}

+public class CapturedAttribute : SA {

+}

+public class NotDelayedAttribute : SA {

+}

+public class NoDefaultContractAttribute : SA {

+}

+public class VerifyAttribute : SA {

+  public VerifyAttribute(bool b) {

+

+  }

+}

+public class StrictReadonlyAttribute : SA {

+}

+public class AdditiveAttribute : SA {

+}

+public class ReadsAttribute : SA {

+  public enum Reads {

+    Nothing,

+    Everything,

+  };

+  public ReadsAttribute(object o) {

+  }

+}

+public class GlobalAccessAttribute : SA {

+  public GlobalAccessAttribute(bool b) {

+  }

+}

+public class EscapesAttribute : SA {

+  public EscapesAttribute(bool b, bool b_2) {

+  }

+}

+public class NeedsContractsAttribute : SA {

+  public NeedsContractsAttribute() {

+  }

+  public NeedsContractsAttribute(bool ret, bool parameters) {

+  }

+  public NeedsContractsAttribute(bool ret, int[] parameters) {

+  }

+}

+public class ImmutableAttribute : SA {

+}

+public class InsideAttribute : SA {

+}

+public class SpecPublicAttribute : SA {

+}

+public class ElementsPeerAttribute : SA {

+}

+public class ResultNotNewlyAllocatedAttribute : SA {

+}

+public class OnceAttribute : SA {

+}
\ No newline at end of file
diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index de0b7227..738e2cf7 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -79,6 +79,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="ProverInterface.cs" />

     <Compile Include="SMTLibLineariser.cs" />

     <Compile Include="TypeDeclCollector.cs" />

diff --git a/Source/Provers/SMTLib/cce.cs b/Source/Provers/SMTLib/cce.cs
new file mode 100644
index 00000000..ef594484
--- /dev/null
+++ b/Source/Provers/SMTLib/cce.cs
@@ -0,0 +1,193 @@
+using System;

+using SA=System.Attribute;

+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 bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

+  //}

+  [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 && Contract.ForAll(collection, pair => NonNullElements(pair));

+  }

+  //[Pure]

+  //public static bool NonNullElements(VariableSeq collection) {

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

+  //}

+  /// <summary>

+  /// For possibly-null lists of non-null elements

+  /// </summary>

+  /// <typeparam name="T"></typeparam>

+  /// <param name="collection"></param>

+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>

+  /// <returns></returns>

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {

+    return (nullability && collection == null) || cce.NonNullElements(collection);

+    //Should be the same as:

+    /*if(nullability&&collection==null)

+     * return true;

+     * return cce.NonNullElements(collection)

+     */

+

+  }

+  [Pure]

+  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {

+    return kvp.Key != null && kvp.Value != null;

+  }

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

+    return iEnumerator != null;

+  }

+  //[Pure]

+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

+  //  return cce.NonNullElements(graph.TopologicalSort());

+  //}

+  [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;

+  }

+  [Pure]

+  public static bool IsNew(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 bool Different(object o, object p) {

+      return true;

+    }

+    [Pure]

+    public static bool New(object o) {

+      return true;

+    }

+  }

+  [Pure]

+  public static void LoopInvariant(bool p) {

+    Contract.Assert(p);

+  }

+  public class UnreachableException : Exception {

+    public UnreachableException() {

+    }

+  }

+  //[Pure]

+  //public static bool IsValid(Microsoft.Dafny.Expression expression) {

+  //  return true;

+  //}

+  //public static List<T> toList<T>(PureCollections.Sequence s) {

+  //  List<T> toRet = new List<T>();

+  //  foreach (T t in s.elems)

+  //    if(t!=null)

+  //    toRet.Add(t);

+  //  return toRet;

+  //}

+

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

+}

+

+public class PeerAttribute : SA {

+}

+public class RepAttribute : SA {

+}

+public class CapturedAttribute : SA {

+}

+public class NotDelayedAttribute : SA {

+}

+public class NoDefaultContractAttribute : SA {

+}

+public class VerifyAttribute : SA {

+  public VerifyAttribute(bool b) {

+

+  }

+}

+public class StrictReadonlyAttribute : SA {

+}

+public class AdditiveAttribute : SA {

+}

+public class ReadsAttribute : SA {

+  public enum Reads {

+    Nothing,

+    Everything,

+  };

+  public ReadsAttribute(object o) {

+  }

+}

+public class GlobalAccessAttribute : SA {

+  public GlobalAccessAttribute(bool b) {

+  }

+}

+public class EscapesAttribute : SA {

+  public EscapesAttribute(bool b, bool b_2) {

+  }

+}

+public class NeedsContractsAttribute : SA {

+  public NeedsContractsAttribute() {

+  }

+  public NeedsContractsAttribute(bool ret, bool parameters) {

+  }

+  public NeedsContractsAttribute(bool ret, int[] parameters) {

+  }

+}

+public class ImmutableAttribute : SA {

+}

+public class InsideAttribute : SA {

+}

+public class SpecPublicAttribute : SA {

+}

+public class ElementsPeerAttribute : SA {

+}

+public class ResultNotNewlyAllocatedAttribute : SA {

+}

+public class OnceAttribute : SA {

+}
\ No newline at end of file
diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj
index 652f8eec..c15ef55a 100644
--- a/Source/Provers/Simplify/Simplify.csproj
+++ b/Source/Provers/Simplify/Simplify.csproj
@@ -73,6 +73,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Let2ImpliesVisitor.cs" />

     <Compile Include="Prover.cs" />

     <Compile Include="ProverInterface.cs" />

@@ -91,8 +92,8 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

-    <ProjectReference Include="..\..\Graph\Graph.sscproj">

-      <Project>{4C28FB90-630E-4B55-A937-11A011B79765}</Project>

+    <ProjectReference Include="..\..\Graph\Graph.csproj">

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">

diff --git a/Source/Provers/Simplify/cce.cs b/Source/Provers/Simplify/cce.cs
new file mode 100644
index 00000000..ef594484
--- /dev/null
+++ b/Source/Provers/Simplify/cce.cs
@@ -0,0 +1,193 @@
+using System;

+using SA=System.Attribute;

+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 bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

+  //}

+  [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 && Contract.ForAll(collection, pair => NonNullElements(pair));

+  }

+  //[Pure]

+  //public static bool NonNullElements(VariableSeq collection) {

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

+  //}

+  /// <summary>

+  /// For possibly-null lists of non-null elements

+  /// </summary>

+  /// <typeparam name="T"></typeparam>

+  /// <param name="collection"></param>

+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>

+  /// <returns></returns>

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {

+    return (nullability && collection == null) || cce.NonNullElements(collection);

+    //Should be the same as:

+    /*if(nullability&&collection==null)

+     * return true;

+     * return cce.NonNullElements(collection)

+     */

+

+  }

+  [Pure]

+  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {

+    return kvp.Key != null && kvp.Value != null;

+  }

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

+    return iEnumerator != null;

+  }

+  //[Pure]

+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

+  //  return cce.NonNullElements(graph.TopologicalSort());

+  //}

+  [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;

+  }

+  [Pure]

+  public static bool IsNew(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 bool Different(object o, object p) {

+      return true;

+    }

+    [Pure]

+    public static bool New(object o) {

+      return true;

+    }

+  }

+  [Pure]

+  public static void LoopInvariant(bool p) {

+    Contract.Assert(p);

+  }

+  public class UnreachableException : Exception {

+    public UnreachableException() {

+    }

+  }

+  //[Pure]

+  //public static bool IsValid(Microsoft.Dafny.Expression expression) {

+  //  return true;

+  //}

+  //public static List<T> toList<T>(PureCollections.Sequence s) {

+  //  List<T> toRet = new List<T>();

+  //  foreach (T t in s.elems)

+  //    if(t!=null)

+  //    toRet.Add(t);

+  //  return toRet;

+  //}

+

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

+}

+

+public class PeerAttribute : SA {

+}

+public class RepAttribute : SA {

+}

+public class CapturedAttribute : SA {

+}

+public class NotDelayedAttribute : SA {

+}

+public class NoDefaultContractAttribute : SA {

+}

+public class VerifyAttribute : SA {

+  public VerifyAttribute(bool b) {

+

+  }

+}

+public class StrictReadonlyAttribute : SA {

+}

+public class AdditiveAttribute : SA {

+}

+public class ReadsAttribute : SA {

+  public enum Reads {

+    Nothing,

+    Everything,

+  };

+  public ReadsAttribute(object o) {

+  }

+}

+public class GlobalAccessAttribute : SA {

+  public GlobalAccessAttribute(bool b) {

+  }

+}

+public class EscapesAttribute : SA {

+  public EscapesAttribute(bool b, bool b_2) {

+  }

+}

+public class NeedsContractsAttribute : SA {

+  public NeedsContractsAttribute() {

+  }

+  public NeedsContractsAttribute(bool ret, bool parameters) {

+  }

+  public NeedsContractsAttribute(bool ret, int[] parameters) {

+  }

+}

+public class ImmutableAttribute : SA {

+}

+public class InsideAttribute : SA {

+}

+public class SpecPublicAttribute : SA {

+}

+public class ElementsPeerAttribute : SA {

+}

+public class ResultNotNewlyAllocatedAttribute : SA {

+}

+public class OnceAttribute : SA {

+}
\ No newline at end of file
diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj
index ba065013..ce7c280e 100644
--- a/Source/Provers/Z3/Z3.csproj
+++ b/Source/Provers/Z3/Z3.csproj
@@ -76,6 +76,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Inspector.cs" />

     <Compile Include="Prover.cs" />

     <Compile Include="ProverInterface.cs" />

diff --git a/Source/Provers/Z3/cce.cs b/Source/Provers/Z3/cce.cs
new file mode 100644
index 00000000..ef594484
--- /dev/null
+++ b/Source/Provers/Z3/cce.cs
@@ -0,0 +1,193 @@
+using System;

+using SA=System.Attribute;

+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 bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

+  //}

+  [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 && Contract.ForAll(collection, pair => NonNullElements(pair));

+  }

+  //[Pure]

+  //public static bool NonNullElements(VariableSeq collection) {

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

+  //}

+  /// <summary>

+  /// For possibly-null lists of non-null elements

+  /// </summary>

+  /// <typeparam name="T"></typeparam>

+  /// <param name="collection"></param>

+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>

+  /// <returns></returns>

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {

+    return (nullability && collection == null) || cce.NonNullElements(collection);

+    //Should be the same as:

+    /*if(nullability&&collection==null)

+     * return true;

+     * return cce.NonNullElements(collection)

+     */

+

+  }

+  [Pure]

+  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {

+    return kvp.Key != null && kvp.Value != null;

+  }

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

+    return iEnumerator != null;

+  }

+  //[Pure]

+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

+  //  return cce.NonNullElements(graph.TopologicalSort());

+  //}

+  [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;

+  }

+  [Pure]

+  public static bool IsNew(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 bool Different(object o, object p) {

+      return true;

+    }

+    [Pure]

+    public static bool New(object o) {

+      return true;

+    }

+  }

+  [Pure]

+  public static void LoopInvariant(bool p) {

+    Contract.Assert(p);

+  }

+  public class UnreachableException : Exception {

+    public UnreachableException() {

+    }

+  }

+  //[Pure]

+  //public static bool IsValid(Microsoft.Dafny.Expression expression) {

+  //  return true;

+  //}

+  //public static List<T> toList<T>(PureCollections.Sequence s) {

+  //  List<T> toRet = new List<T>();

+  //  foreach (T t in s.elems)

+  //    if(t!=null)

+  //    toRet.Add(t);

+  //  return toRet;

+  //}

+

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

+}

+

+public class PeerAttribute : SA {

+}

+public class RepAttribute : SA {

+}

+public class CapturedAttribute : SA {

+}

+public class NotDelayedAttribute : SA {

+}

+public class NoDefaultContractAttribute : SA {

+}

+public class VerifyAttribute : SA {

+  public VerifyAttribute(bool b) {

+

+  }

+}

+public class StrictReadonlyAttribute : SA {

+}

+public class AdditiveAttribute : SA {

+}

+public class ReadsAttribute : SA {

+  public enum Reads {

+    Nothing,

+    Everything,

+  };

+  public ReadsAttribute(object o) {

+  }

+}

+public class GlobalAccessAttribute : SA {

+  public GlobalAccessAttribute(bool b) {

+  }

+}

+public class EscapesAttribute : SA {

+  public EscapesAttribute(bool b, bool b_2) {

+  }

+}

+public class NeedsContractsAttribute : SA {

+  public NeedsContractsAttribute() {

+  }

+  public NeedsContractsAttribute(bool ret, bool parameters) {

+  }

+  public NeedsContractsAttribute(bool ret, int[] parameters) {

+  }

+}

+public class ImmutableAttribute : SA {

+}

+public class InsideAttribute : SA {

+}

+public class SpecPublicAttribute : SA {

+}

+public class ElementsPeerAttribute : SA {

+}

+public class ResultNotNewlyAllocatedAttribute : SA {

+}

+public class OnceAttribute : SA {

+}
\ No newline at end of file
diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj
index 05b12234..b2f61e8c 100644
--- a/Source/VCExpr/VCExpr.csproj
+++ b/Source/VCExpr/VCExpr.csproj
@@ -75,6 +75,7 @@
   <ItemGroup>

     <Compile Include="BigLiteralAbstracter.cs" />

     <Compile Include="Boogie2VCExpr.cs" />

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

     <Compile Include="Clustering.cs" />

     <Compile Include="LetBindingSorter.cs" />

     <Compile Include="NameClashResolver.cs" />

diff --git a/Source/VCExpr/cce.cs b/Source/VCExpr/cce.cs
index ff619b7c..ef594484 100644
--- a/Source/VCExpr/cce.cs
+++ b/Source/VCExpr/cce.cs
@@ -1,14 +1,19 @@
 using System;

+using SA=System.Attribute;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Text;

-using Microsoft.Boogie;

+//using Microsoft.Boogie;

 

-  /// <summary>

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

-    /// </summary>

+/// <summary>

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

+/// </summary>

 

 public static class cce {

+  //[Pure]

+  //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

+  //}

   [Pure]

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

     Contract.Assert(t != null);

@@ -22,20 +27,39 @@ public static class cce {
   public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {

     return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));

   }

-  [Pure]

-  public static bool NonNullElements(VariableSeq collection) {

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

-  }

   //[Pure]

-  //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

-  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

+  //public static bool NonNullElements(VariableSeq collection) {

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

   //}

+  /// <summary>

+  /// For possibly-null lists of non-null elements

+  /// </summary>

+  /// <typeparam name="T"></typeparam>

+  /// <param name="collection"></param>

+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>

+  /// <returns></returns>

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {

+    return (nullability && collection == null) || cce.NonNullElements(collection);

+    //Should be the same as:

+    /*if(nullability&&collection==null)

+     * return true;

+     * return cce.NonNullElements(collection)

+     */

 

+  }

   [Pure]

   public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {

     return kvp.Key != null && kvp.Value != null;

   }

-

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

+    return iEnumerator != null;

+  }

+  //[Pure]

+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

+  //  return cce.NonNullElements(graph.TopologicalSort());

+  //}

   [Pure]

   public static void BeginExpose(object o) {

   }

@@ -58,6 +82,10 @@ public static class cce {
   public static bool IsExposed(object o) {

     return true;

   }

+  [Pure]

+  public static bool IsNew(object o) {

+    return true;

+  }

   public static class Owner {

     [Pure]

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

@@ -74,12 +102,19 @@ public static class cce {
     public static bool None(object o) {

       return true;

     }

+    [Pure]

+    public static bool Different(object o, object p) {

+      return true;

+    }

+    [Pure]

+    public static bool New(object o) {

+      return true;

+    }

   }

   [Pure]

   public static void LoopInvariant(bool p) {

     Contract.Assert(p);

   }

-

   public class UnreachableException : Exception {

     public UnreachableException() {

     }

@@ -88,43 +123,71 @@ public static class cce {
   //public static bool IsValid(Microsoft.Dafny.Expression expression) {

   //  return true;

   //}

+  //public static List<T> toList<T>(PureCollections.Sequence s) {

+  //  List<T> toRet = new List<T>();

+  //  foreach (T t in s.elems)

+  //    if(t!=null)

+  //    toRet.Add(t);

+  //  return toRet;

+  //}

 

-  internal static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

-    return iEnumerator != null;

-  }

+  //internal static bool NonNullElements(Set set) {

+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

+  //}

 }

 

-public class PeerAttribute : System.Attribute {

+public class PeerAttribute : SA {

 }

-public class RepAttribute : System.Attribute {

+public class RepAttribute : SA {

 }

-public class CapturedAttribute : System.Attribute {

+public class CapturedAttribute : SA {

 }

-public class NotDelayedAttribute : System.Attribute {

+public class NotDelayedAttribute : SA {

 }

-public class NoDefaultContractAttribute : System.Attribute {

+public class NoDefaultContractAttribute : SA {

 }

-public class VerifyAttribute : System.Attribute {

+public class VerifyAttribute : SA {

   public VerifyAttribute(bool b) {

 

   }

 }

-public class StrictReadonlyAttribute : System.Attribute {

- }

-public class AdditiveAttribute : System.Attribute {

+public class StrictReadonlyAttribute : SA {

+}

+public class AdditiveAttribute : SA {

 }

-public class ReadsAttribute : System.Attribute {

+public class ReadsAttribute : SA {

   public enum Reads {

     Nothing,

+    Everything,

   };

   public ReadsAttribute(object o) {

   }

 }

-public class GlobalAccessAttribute : System.Attribute {

+public class GlobalAccessAttribute : SA {

   public GlobalAccessAttribute(bool b) {

   }

 }

-public class EscapesAttribute : System.Attribute {

+public class EscapesAttribute : SA {

   public EscapesAttribute(bool b, bool b_2) {

   }

+}

+public class NeedsContractsAttribute : SA {

+  public NeedsContractsAttribute() {

+  }

+  public NeedsContractsAttribute(bool ret, bool parameters) {

+  }

+  public NeedsContractsAttribute(bool ret, int[] parameters) {

+  }

+}

+public class ImmutableAttribute : SA {

+}

+public class InsideAttribute : SA {

+}

+public class SpecPublicAttribute : SA {

+}

+public class ElementsPeerAttribute : SA {

+}

+public class ResultNotNewlyAllocatedAttribute : SA {

+}

+public class OnceAttribute : SA {

 }
\ No newline at end of file
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index d6890363..d06cb13f 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -77,6 +77,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Check.cs" />

     <Compile Include="ConditionGeneration.cs" />

     <Compile Include="Context.cs" />

@@ -101,8 +102,8 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

-    <ProjectReference Include="..\Graph\Graph.sscproj">

-      <Project>{4C28FB90-630E-4B55-A937-11A011B79765}</Project>

+    <ProjectReference Include="..\Graph\Graph.csproj">

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

     <ProjectReference Include="..\VCExpr\VCExpr.csproj">