diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/AIFramework/AIFramework.csproj | 7 | ||||
| -rw-r--r-- | Source/AbsInt/AbsInt.csproj | 5 | ||||
| -rw-r--r-- | Source/Basetypes/Basetypes.csproj | 7 | ||||
| -rw-r--r-- | Source/Basetypes/cce.cs | 2 | ||||
| -rw-r--r-- | Source/Boogie.sln | 12 | ||||
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 8 | ||||
| -rw-r--r-- | Source/CodeContractsExtender/CodeContractsExtender.csproj | 67 | ||||
| -rw-r--r-- | Source/CodeContractsExtender/cce.cs | 193 | ||||
| -rw-r--r-- | Source/Core/Core.csproj | 5 | ||||
| -rw-r--r-- | Source/Graph/Graph.csproj | 9 | ||||
| -rw-r--r-- | Source/Provers/Isabelle/Isabelle.csproj | 5 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLib.csproj | 5 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Simplify.csproj | 5 | ||||
| -rw-r--r-- | Source/Provers/Z3/Z3.csproj | 5 | ||||
| -rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 5 | ||||
| -rw-r--r-- | Source/VCExpr/VCExpr.csproj | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/VCGeneration.csproj | 5 |
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<T!>?, rather than an IEnumerable<T!>!</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>
|