Boogie: Changed the cce classes into one separate project, which every other project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.

17 files changed, 332 insertions, 18 deletions

diff --git a/Source/AIFramework/AIFramework.csproj b/Source/AIFramework/AIFramework.csproj
index 1a10628c..0e5804d7 100644
--- a/Source/AIFramework/AIFramework.csproj
+++ b/Source/AIFramework/AIFramework.csproj
@@ -70,9 +70,6 @@
     <Reference Include="System" />

   </ItemGroup>

   <ItemGroup>

-    <Compile Include="cce.cs">

-      <SubType>Code</SubType>

-    </Compile>

     <Compile Include="CommonFunctionSymbols.cs" />

     <Compile Include="Expr.cs" />

     <Compile Include="Functional.cs" />

@@ -96,6 +93,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

   </ItemGroup>

   <ItemGroup>

     <Folder Include="Properties\" />

diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index a2d8e1cc..66dd256e 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -81,7 +81,6 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="AbstractInterpretation.cs" />

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

     <Compile Include="ExprFactories.cs" />

     <Compile Include="LoopInvariantsOnDemand.cs" />

     <Compile Include="Traverse.cs" />

@@ -96,6 +95,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index eed8639e..b732f818 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -81,11 +81,16 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BigNum.cs" />

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

     <Compile Include="Rational.cs" />

     <Compile Include="Set.cs" />

   </ItemGroup>

   <ItemGroup>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

     <Folder Include="Properties\" />

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

diff --git a/Source/Basetypes/cce.cs b/Source/Basetypes/cce.cs
index d85a1300..ef594484 100644
--- a/Source/Basetypes/cce.cs
+++ b/Source/Basetypes/cce.cs
@@ -131,7 +131,7 @@ public static class cce {
   //  return toRet;

   //}

 

-  //internal static bool NonNullElements(Microsoft.Boogie.Set set) {

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

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

   //}

 }

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 4e81b080..06ef58fa 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -29,6 +29,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "Graph\Graph.csproj
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Basetypes", "Basetypes\Basetypes.csproj", "{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "CodeContractsExtender\CodeContractsExtender.csproj", "{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|.NET = Debug|.NET

@@ -176,6 +178,16 @@ Global
 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.Build.0 = Release|Any CPU

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Release|.NET.ActiveCfg = Release|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Release|Any CPU.Build.0 = Release|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.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 a5fb46f6..6161cc57 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -87,7 +87,6 @@
   <ItemGroup>

     <Compile Include="BoogieDriver.cs" />

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

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

   </ItemGroup>

   <ItemGroup>

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

@@ -102,6 +101,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

@@ -136,6 +139,9 @@
     </ProjectReference>

   </ItemGroup>

   <ItemGroup>

+    <WCFMetadata Include="Service References\" />

+  </ItemGroup>

+  <ItemGroup>

     <Folder Include="Properties\" />

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj
new file mode 100644
index 00000000..46edbd5e
--- /dev/null
+++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj
@@ -0,0 +1,67 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="3.5" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProductVersion>9.0.30729</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>CodeContractsExtender</RootNamespace>

+    <AssemblyName>CodeContractsExtender</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <SignAssembly>true</SignAssembly>

+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\Microsoft.Contracts.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Core">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+    <Reference Include="System.Xml.Linq">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+    <Reference Include="System.Data.DataSetExtensions">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

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

+  </ItemGroup>

+  <ItemGroup>

+    <Folder Include="Properties\" />

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>
\ No newline at end of file
diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs
new file mode 100644
index 00000000..ef594484
--- /dev/null
+++ b/Source/CodeContractsExtender/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/Core/Core.csproj b/Source/Core/Core.csproj
index 49ad3c7e..fb9252be 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -92,7 +92,6 @@
     <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" />

@@ -122,6 +121,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

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

       <Name>Graph</Name>

diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj
index c2d3e5b0..1756b36f 100644
--- a/Source/Graph/Graph.csproj
+++ b/Source/Graph/Graph.csproj
@@ -76,12 +76,15 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

-    <Compile Include="cce.cs">

-      <SubType>Code</SubType>

-    </Compile>

     <Compile Include="Graph.cs" />

   </ItemGroup>

   <ItemGroup>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

     <Folder Include="Properties\" />

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

diff --git a/Source/Provers/Isabelle/Isabelle.csproj b/Source/Provers/Isabelle/Isabelle.csproj
index a37eba66..2db71715 100644
--- a/Source/Provers/Isabelle/Isabelle.csproj
+++ b/Source/Provers/Isabelle/Isabelle.csproj
@@ -69,7 +69,6 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Prover.cs" />

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

   </ItemGroup>

@@ -82,6 +81,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index b30e873b..fd83f893 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -79,7 +79,6 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="ProverInterface.cs" />

     <Compile Include="SMTLibLineariser.cs" />

     <Compile Include="TypeDeclCollector.cs" />

@@ -94,6 +93,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj
index 9591278f..368f6723 100644
--- a/Source/Provers/Simplify/Simplify.csproj
+++ b/Source/Provers/Simplify/Simplify.csproj
@@ -73,7 +73,6 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Let2ImpliesVisitor.cs" />

     <Compile Include="Prover.cs" />

     <Compile Include="ProverInterface.cs" />

@@ -88,6 +87,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj
index 05ff9d9a..8755d6c2 100644
--- a/Source/Provers/Z3/Z3.csproj
+++ b/Source/Provers/Z3/Z3.csproj
@@ -76,7 +76,6 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Inspector.cs" />

     <Compile Include="Prover.cs" />

     <Compile Include="ProverInterface.cs" />

@@ -92,6 +91,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index a951715b..1aa4534f 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -69,6 +69,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

@@ -91,7 +95,6 @@
     </ProjectReference>

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="ContextLayer.cs" />

     <Compile Include="ProverLayer.cs" />

     <Compile Include="SafeContext.cs" />

diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj
index e9209c8a..9de26941 100644
--- a/Source/VCExpr/VCExpr.csproj
+++ b/Source/VCExpr/VCExpr.csproj
@@ -75,7 +75,6 @@
   <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" />

@@ -97,6 +96,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 37b6fe60..b6954926 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -77,7 +77,6 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Check.cs" />

     <Compile Include="ConditionGeneration.cs" />

     <Compile Include="Context.cs" />

@@ -98,6 +97,10 @@
       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>