Fixed test failures in the "Checked" configuration.

4 files changed, 102 insertions, 7 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index ca707746..adaf7cf3 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -502,8 +502,8 @@ Global
 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|x86.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

@@ -520,13 +520,13 @@ Global
 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|.NET.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

-		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|.NET.ActiveCfg = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Release|x86

-		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Checked|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Checked|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Release|x86

 		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|.NET.ActiveCfg = Debug|x86

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index cb0ca968..6609c43f 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1397,7 +1397,7 @@ namespace Microsoft.Boogie {
       : base(tok, typedIdent) {

       Contract.Requires(tok != null);

       Contract.Requires(typedIdent != null);

-      Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);

+      Contract.Requires(typedIdent.Name != null && (!typedIdent.HasName || typedIdent.Name.Length > 0));

       Contract.Requires(typedIdent.WhereExpr == null);

       // base(tok, typedIdent);

       this.Unique = true;

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 407ebe5f..5eb3dc52 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -13,6 +13,22 @@
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

     <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

+    <PublishUrl>publish\</PublishUrl>

+    <Install>true</Install>

+    <InstallFrom>Disk</InstallFrom>

+    <UpdateEnabled>false</UpdateEnabled>

+    <UpdateMode>Foreground</UpdateMode>

+    <UpdateInterval>7</UpdateInterval>

+    <UpdateIntervalUnits>Days</UpdateIntervalUnits>

+    <UpdatePeriodically>false</UpdatePeriodically>

+    <UpdateRequired>false</UpdateRequired>

+    <MapFileExtensions>true</MapFileExtensions>

+    <ApplicationRevision>0</ApplicationRevision>

+    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>

+    <IsWebBootstrapper>false</IsWebBootstrapper>

+    <UseApplicationTrust>false</UseApplicationTrust>

+    <BootstrapperEnabled>true</BootstrapperEnabled>

   </PropertyGroup>

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

     <PlatformTarget>x86</PlatformTarget>

@@ -33,6 +49,34 @@
     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

   </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">

+    <OutputPath>bin\x86\Checked\</OutputPath>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

@@ -75,6 +119,28 @@
       <Name>ParserHelper</Name>

     </ProjectReference>

   </ItemGroup>

+  <ItemGroup>

+    <BootstrapperPackage Include=".NETFramework,Version=v4.0,Profile=Client">

+      <Visible>False</Visible>

+      <ProductName>Microsoft .NET Framework 4 Client Profile %28x86 and x64%29</ProductName>

+      <Install>true</Install>

+    </BootstrapperPackage>

+    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">

+      <Visible>False</Visible>

+      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>

+      <Install>false</Install>

+    </BootstrapperPackage>

+    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">

+      <Visible>False</Visible>

+      <ProductName>.NET Framework 3.5 SP1</ProductName>

+      <Install>false</Install>

+    </BootstrapperPackage>

+    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">

+      <Visible>False</Visible>

+      <ProductName>Windows Installer 3.1</ProductName>

+      <Install>true</Install>

+    </BootstrapperPackage>

+  </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.

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index b87f68d7..bc7bb8c8 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -12,6 +12,7 @@
     <AssemblyName>Houdini</AssemblyName>

     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -36,6 +37,34 @@
   <PropertyGroup>

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

   </PropertyGroup>

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

+    <OutputPath>bin\Checked\</OutputPath>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />