diff options
author | qadeer <unknown> | 2010-12-01 05:43:17 +0000 |
---|---|---|
committer | qadeer <unknown> | 2010-12-01 05:43:17 +0000 |
commit | 5db34109bbb72d290239dfdb571d321fe3f1c48c (patch) | |
tree | 50c5ba304226e584a8cbf7c03a7480a3d0a65def /Source/VCExpr | |
parent | 95ff970b12779a1c0e814084100a0e88e6cc1c3d (diff) |
Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln
Diffstat (limited to 'Source/VCExpr')
-rw-r--r-- | Source/VCExpr/TypeErasureArguments.cs | 4 | ||||
-rw-r--r-- | Source/VCExpr/VCExpr.csproj | 4 |
2 files changed, 2 insertions, 6 deletions
diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index c63a158f..6cc021fa 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -227,8 +227,8 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); storeTypes[i] = abstractedType;
else
storeTypes[i] = AxBuilder.U;
- Microsoft.Contracts.NonNullType.AssertInitialized(selectTypes);
- Microsoft.Contracts.NonNullType.AssertInitialized(storeTypes);
+ Contract.Assert(cce.NonNullElements<Type>(selectTypes));
+ Contract.Assert(cce.NonNullElements<Type>(storeTypes));
select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes);
store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes);
diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj index 382a6694..116112a0 100644 --- a/Source/VCExpr/VCExpr.csproj +++ b/Source/VCExpr/VCExpr.csproj @@ -100,10 +100,6 @@ </PropertyGroup>
<ItemGroup>
<Reference Include="System" />
- <Reference Include="System.Compiler.Runtime, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>
- </Reference>
<Reference Include="System.Data" />
<Reference Include="System.Xml" />
</ItemGroup>
|