Dafny: Added a 'Checked' configuration and fixed some runtime assertion violations.

1 files changed, 53 insertions, 18 deletions

diff --git a/DafnyDriver/DafnyDriver.csproj b/DafnyDriver/DafnyDriver.csproj
index cf88eed4..5dac8f59 100644
--- a/DafnyDriver/DafnyDriver.csproj
+++ b/DafnyDriver/DafnyDriver.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

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

   <PropertyGroup>

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

@@ -19,6 +19,8 @@
     </FileUpgradeFlags>

     <OldToolsVersion>3.5</OldToolsVersion>

     <UpgradeBackupLocation />

+    <IsWebBootstrapper>false</IsWebBootstrapper>

+    <TargetFrameworkProfile />

     <PublishUrl>publish\</PublishUrl>

     <Install>true</Install>

     <InstallFrom>Disk</InstallFrom>

@@ -31,10 +33,8 @@
     <MapFileExtensions>true</MapFileExtensions>

     <ApplicationRevision>0</ApplicationRevision>

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

-    <IsWebBootstrapper>false</IsWebBootstrapper>

     <UseApplicationTrust>false</UseApplicationTrust>

     <BootstrapperEnabled>true</BootstrapperEnabled>

-    <TargetFrameworkProfile />

   </PropertyGroup>

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

     <DebugSymbols>true</DebugSymbols>

@@ -72,8 +72,12 @@
     <CodeContractsBaseLineFile>

     </CodeContractsBaseLineFile>

     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

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

     <DebugType>pdbonly</DebugType>

@@ -84,29 +88,60 @@
     <WarningLevel>4</WarningLevel>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

   </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

+    <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="AbsInt, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\AbsInt\bin\Debug\AbsInt.dll</HintPath>

+    <Reference Include="AbsInt">

+      <HintPath>..\..\Binaries\AbsInt.dll</HintPath>

     </Reference>

-    <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\AIFramework\bin\debug\AIFramework.dll</HintPath>

+    <Reference Include="AIFramework">

+      <HintPath>..\..\Binaries\AIFramework.dll</HintPath>

     </Reference>

-    <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\Core\bin\Debug\Core.dll</HintPath>

+    <Reference Include="Core">

+      <HintPath>..\..\Binaries\Core.dll</HintPath>

     </Reference>

-    <Reference Include="ParserHelper, Version=0.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+    <Reference Include="ParserHelper, Version=2.2.30705.1126, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\ParserHelper.dll</HintPath>

     </Reference>

     <Reference Include="System" />

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

-    <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\VCGeneration\bin\debug\VCGeneration.dll</HintPath>

+    <Reference Include="VCGeneration">

+      <HintPath>..\..\Binaries\VCGeneration.dll</HintPath>

     </Reference>

   </ItemGroup>

   <ItemGroup>

@@ -147,4 +182,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file