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

7 files changed, 136 insertions, 44 deletions

diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index 9e99e4bc..034dfd7b 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -7,6 +7,9 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyPipeline", "Dafny\Dafn
 EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

+		Checked|.NET = Checked|.NET

+		Checked|Any CPU = Checked|Any CPU

+		Checked|Mixed Platforms = Checked|Mixed Platforms

 		Debug|.NET = Debug|.NET

 		Debug|Any CPU = Debug|Any CPU

 		Debug|Mixed Platforms = Debug|Mixed Platforms

@@ -15,6 +18,12 @@ Global
 		Release|Mixed Platforms = Release|Mixed Platforms

 	EndGlobalSection

 	GlobalSection(ProjectConfigurationPlatforms) = postSolution

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|.NET.ActiveCfg = Checked|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|.NET.Build.0 = Checked|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Any CPU.ActiveCfg = Debug|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Any CPU.Build.0 = Debug|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|.NET.Build.0 = Debug|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

@@ -26,6 +35,12 @@ Global
 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Any CPU.Build.0 = Release|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|.NET.ActiveCfg = Checked|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|.NET.Build.0 = Checked|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Any CPU.ActiveCfg = Debug|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Any CPU.Build.0 = Debug|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU

+		{FE44674A-1633-4917-99F4-57635E6FA740}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.Build.0 = Debug|Any CPU

 		{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 218f95e5..0a553036 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(module != null);

       Contract.Requires(cce.NonNullElements(typeArgs));

       Contract.Requires(cce.NonNullElements(ctors));

-      Contract.Invariant(1 <= ctors.Count);

+      Contract.Requires(1 <= ctors.Count);

       Ctors = ctors;

     }

   }

@@ -871,8 +871,8 @@ namespace Microsoft.Dafny {
     void ObjectInvariant() {

       Contract.Invariant(Expr != null);

       Contract.Invariant(cce.NonNullElements(Toks));

-      Contract.Invariant(cce.NonNullElements(Formals));

-      Contract.Invariant(cce.NonNullElements(Refined));

+      Contract.Invariant(Formals == null || cce.NonNullElements(Formals));

+      Contract.Invariant(Refined == null || cce.NonNullElements(Refined));

     }

 

 

@@ -1298,12 +1298,13 @@ namespace Microsoft.Dafny {
     public Statement TargetStmt;  // filled in during resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(TargetLabel == null || 1 <= BreakCount);

+      Contract.Invariant(TargetLabel != null || 1 <= BreakCount);

     }

 

     public BreakStmt(IToken tok, string targetLabel)

       : base(tok) {

       Contract.Requires(tok != null);

+      Contract.Requires(targetLabel != null);

       this.TargetLabel = targetLabel;

     }

     public BreakStmt(IToken tok, int breakCount)

@@ -1639,13 +1640,11 @@ namespace Microsoft.Dafny {
     public IfStmt(IToken tok, Expression guard, Statement thn, Statement els)

       : base(tok) {

       Contract.Requires(tok != null);

-      Contract.Requires(guard != null);

       Contract.Requires(thn != null);

       Contract.Requires(els == null || els is BlockStmt || els is IfStmt);

       this.Guard = guard;

       this.Thn = thn;

       this.Els = els;

-

     }

   }

 

@@ -1875,9 +1874,15 @@ namespace Microsoft.Dafny {
       Contract.Invariant(tok != null);

     }

 

+    [Pure]

+    public bool WasResolved()

+    {

+      return Type != null;

+    }

+

     public Expression Resolved {

       get {

-        Contract.Requires(type != null);  // should be called only on resolved expressions; this approximates that precondition

+        Contract.Requires(WasResolved());  // should be called only on resolved expressions; this approximates that precondition

         Expression r = this;

         while (true) {

           var rr = r as ConcreteSyntaxExpression;

@@ -1899,7 +1904,7 @@ namespace Microsoft.Dafny {
       [NoDefaultContract]  // no particular validity of 'this' is required, except that it not be committed

       set {

         Contract.Requires(cce.IsValid(this));

-        Contract.Requires(Type == null);  // set it only once

+        Contract.Requires(!WasResolved());  // set it only once

         Contract.Requires(value != null);

         //modifies type;

         type = value.Normalize();

@@ -2907,7 +2912,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(operands != null);

       Contract.Requires(operators != null);

       Contract.Requires(desugaring != null);

-      Contract.Requires(operators.Count == operators.Count + 1);

+      Contract.Requires(operands.Count == operators.Count + 1);

 

       Operands = operands;

       Operators = operators;

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 6a15b1f7..40a8cacc 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.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>

@@ -75,6 +75,10 @@
     <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

     <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>

@@ -85,6 +89,43 @@
     <WarningLevel>4</WarningLevel>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

   </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

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

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>

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

       <SpecificVersion>False</SpecificVersion>

@@ -154,4 +195,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 34fcb740..97324ef9 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -723,7 +723,7 @@ namespace Microsoft.Dafny {
             }

             wr.Write(")");

           }

-          bool parensNeeded = !isLastCase && mc.Body.Resolved is MatchExpr;

+          bool parensNeeded = !isLastCase && mc.Body.WasResolved() && mc.Body.Resolved is MatchExpr;

           if (parensNeeded) {

             wr.WriteLine(" => (");

           } else {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 5e2bc911..b9f5e7e6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -935,9 +935,9 @@ namespace Microsoft.Dafny {
       Contract.Requires(proxy != null);

       Contract.Requires(t != null);

       Contract.Requires(proxy.T == null);

-      Contract.Requires((t is TypeProxy)|| ((TypeProxy)t).T == null);

+      Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null);

       //modifies proxy.T, ((TypeProxy)t).T;  // might also change t.T if t is a proxy

-      Contract.Ensures(Contract.Result<bool>() || proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null));

+      Contract.Ensures(Contract.Result<bool>() == (proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null)));

       if (proxy == t) {

         // they are already in the same equivalence class

         return true;

@@ -1845,7 +1845,7 @@ namespace Microsoft.Dafny {
         Contract.Assume(lhs.Type != null);  // a sanity check that LHSs have already been resolved

       }

       // resolve arguments

-      if (!s.IsGhost) {

+      if (!s.IsGhost && s.Receiver.WasResolved()) {

         CheckIsNonGhost(s.Receiver);

       }

       int j = 0;

@@ -2791,7 +2791,7 @@ namespace Microsoft.Dafny {
     void CheckIsNonGhost(Expression expr) {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

-      Contract.Requires(expr.Type != null);  // this check approximates the requirement that "expr" be resolved

+      Contract.Requires(expr.WasResolved());  // this check approximates the requirement that "expr" be resolved

 

       if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

@@ -3505,7 +3505,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

 

-      if (expr is ThisExpr) {

+      if (expr is ThisExpr && !expr.WasResolved()) {

         // Allow 'this' here, regardless of scope.AllowInstance.  The caller is responsible for

         // making sure 'this' does not really get used when it's not available.

         expr.Type = GetThisType(expr.tok, currentClass);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 17df4e06..3ec3c291 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2751,10 +2751,9 @@ namespace Microsoft.Dafny {
 

       public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)

       {

-        Contract.Requires(node != null);

         Contract.Ensures(Contract.Result<Expr>() != null);

 

-        if (subst.ContainsKey(node.Name))

+        if (node != null && subst.ContainsKey(node.Name))

           return subst[node.Name];

         else

           return base.VisitIdentifierExpr(node);

@@ -3582,7 +3581,7 @@ namespace Microsoft.Dafny {
     void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,

                         Bpl.StmtListBuilder builder, VariableSeq locals, ExpressionTranslator etran) {

       Contract.Requires(alternatives != null);

-      Contract.Requires((elseCase0 == null) == (elseCase1 == null));  // ugly way of doing a type union

+      Contract.Requires((elseCase0 != null) == (elseCase1 == null));  // ugly way of doing a type union

       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

@@ -3665,7 +3664,7 @@ namespace Microsoft.Dafny {
       Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {

 

       Contract.Requires(tok != null);

-      Contract.Requires((dafnyReceiver == null) != (bReceiver == null));

+      Contract.Requires((dafnyReceiver != null) || (bReceiver != null));

       Contract.Requires(method != null);

       Contract.Requires(cce.NonNullElements(Args));

       Contract.Requires(cce.NonNullElements(Lhss));

@@ -4515,7 +4514,7 @@ namespace Microsoft.Dafny {
       public readonly string This;

       public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.

       readonly Function applyLimited_CurrentFunction;

-      readonly int layerOffset = 0;

+      public readonly int layerOffset = 0;

       public int Statistics_FunctionCount = 0;

       [ContractInvariantMethod]

       void ObjectInvariant()

@@ -4564,7 +4563,6 @@ namespace Microsoft.Dafny {
           Contract.Requires(translator != null);

           Contract.Requires(predef != null);

           Contract.Requires(heap != null);

-          Contract.Requires(applyLimited_CurrentFunction != null);

           this.translator = translator;

           this.predef = predef;

           this.HeapExpr = heap;

@@ -6271,7 +6269,6 @@ namespace Microsoft.Dafny {
 

     static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(expr != null);

-      Contract.Requires(receiverReplacement != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(Contract.Result<Expression>() != null);

 

@@ -6436,8 +6433,7 @@ namespace Microsoft.Dafny {
     static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,

                                                  Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(cce.NonNullElements(elist));

-      Contract.Requires((receiverReplacement == null) == (substMap == null));

-      Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));

+      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));

 

       List<Expression> newElist = null;  // initialized lazily

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index cf88eed4..5dac8f59 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/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