diff options
| author |  wuestholz <unknown> | 2013-08-05 10:23:41 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-08-05 10:23:41 -0700 |
| commit | f89732676bc18182314f91a77821e2194a2616dc (patch) | |
| tree | 3066125d01b810ee26382098629995fac7e13616 /Source | |
| parent | d5a32ffd75e5723a5f2a6f9d6a5b50b3e692a0ff (diff) | |
Fixed several build errors in the 'Checked' configuration.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BVD/BVD.csproj | 2 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 2 | ||||
| -rw-r--r-- | Source/Doomed/Doomed.csproj | 35 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.csproj | 37 | ||||
| -rw-r--r-- | Source/Model/Model.csproj | 6 | ||||
| -rw-r--r-- | Source/ModelViewer/ModelViewer.csproj | 4 | ||||
| -rw-r--r-- | Source/Predication/Predication.csproj | 35 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 12 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
11 files changed, 126 insertions, 13 deletions
diff --git a/Source/BVD/BVD.csproj b/Source/BVD/BVD.csproj index 448adff7..687e83fb 100644 --- a/Source/BVD/BVD.csproj +++ b/Source/BVD/BVD.csproj @@ -42,7 +42,7 @@ <PlatformTarget>AnyCPU</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 2817acdc..7b3f6fc5 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2924,7 +2924,7 @@ namespace Microsoft.Boogie { this.formalMap = null;
}
public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() {
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<Variable, Expr>>() != null);
if (this.formalMap != null)
return this.formalMap;
diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj index a2390a39..e83c8f30 100644 --- a/Source/Doomed/Doomed.csproj +++ b/Source/Doomed/Doomed.csproj @@ -14,6 +14,7 @@ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
<ProductVersion>12.0.0</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -31,6 +32,40 @@ <DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>true</SignAssembly>
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index bebe686d..3c50afae 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -16,6 +16,7 @@ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
<ProductVersion>12.0.0</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -29,10 +30,44 @@ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj index cfd5f852..b307a799 100644 --- a/Source/Model/Model.csproj +++ b/Source/Model/Model.csproj @@ -19,7 +19,7 @@ <DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
@@ -27,7 +27,7 @@ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
@@ -40,7 +40,7 @@ </PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<DebugType>full</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index 30f444c6..f86e4d4f 100644 --- a/Source/ModelViewer/ModelViewer.csproj +++ b/Source/ModelViewer/ModelViewer.csproj @@ -44,7 +44,7 @@ <PlatformTarget>AnyCPU</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
@@ -60,7 +60,7 @@ </PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">
<DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\Checked\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<DebugType>full</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj index 663de263..9ed46bc6 100644 --- a/Source/Predication/Predication.csproj +++ b/Source/Predication/Predication.csproj @@ -14,6 +14,7 @@ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
<ProductVersion>12.0.0</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -31,6 +32,40 @@ <DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>true</SignAssembly>
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 62451caa..2237c2fc 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -57,7 +57,7 @@ namespace Microsoft.Boogie { public void GetReady()
{
- Contract.Requires(status == CheckerStatus.Idle);
+ Contract.Requires(IsIdle);
status = CheckerStatus.Ready;
}
@@ -268,6 +268,14 @@ namespace Microsoft.Boogie { }
}
+ public bool IsReady
+ {
+ get
+ {
+ return status == CheckerStatus.Ready;
+ }
+ }
+
public bool IsClosed {
get {
return status == CheckerStatus.Closed;
@@ -334,7 +342,7 @@ namespace Microsoft.Boogie { Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
- Contract.Requires(status == CheckerStatus.Ready);
+ Contract.Requires(IsReady);
status = CheckerStatus.Busy;
hasOutput = false;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 36b8fbe5..0ea08356 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1191,7 +1191,7 @@ namespace VC { protected Dictionary<Variable, Expr> ComputeIncarnationMap(Block b, Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation) {
Contract.Requires(b != null);
Contract.Requires(block2Incarnation != null);
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<Variable, Expr>>() != null);
if (b.Predecessors.Count == 0) {
return new Dictionary<Variable, Expr>();
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 7f5b3779..ceea2477 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2117,7 +2117,7 @@ namespace VC { }
public Dictionary<int, Absy> getLabel2absy() {
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<int, Absy>>() != null);
Contract.Assert(currProc != null);
if (currProc == "") {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index fd7a4f72..4806318a 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2121,7 +2121,7 @@ namespace VC { {
Contract.Requires(impl != null);
Contract.Requires(program != null);
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Dictionary<TransferCmd, ReturnCmd>>() != null);
Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
|