diff options
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 212 | ||||
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 646 | ||||
| -rw-r--r-- | Source/BoogieDriver/cce.cs | 210 |
3 files changed, 534 insertions, 534 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index fa038803..be88a745 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -1,106 +1,106 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-//---------------------------------------------------------------------------------------------
-// OnlyBoogie OnlyBoogie.ssc
-// - main program for taking a BPL program and verifying it
-//---------------------------------------------------------------------------------------------
-
-namespace Microsoft.Boogie {
- using System;
- using System.IO;
- using System.Collections.Generic;
- using System.Diagnostics.Contracts;
-
- /*
- The following assemblies are referenced because they are needed at runtime, not at compile time:
- BaseTypes
- Provers.Z3
- System.Compiler.Framework
- */
-
- public class OnlyBoogie
- {
-
- public static int Main(string[] args)
- {
- Contract.Requires(cce.NonNullElements(args));
-
- ExecutionEngine.printer = new ConsolePrinter();
-
- CommandLineOptions.Install(new CommandLineOptions());
-
- CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
- if (!CommandLineOptions.Clo.Parse(args)) {
- goto END;
- }
- if (CommandLineOptions.Clo.Files.Count == 0) {
- ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified.");
- goto END;
- }
- if (CommandLineOptions.Clo.XmlSink != null) {
- string errMsg = CommandLineOptions.Clo.XmlSink.Open();
- if (errMsg != null) {
- ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg);
- goto END;
- }
- }
- if (!CommandLineOptions.Clo.DontShowLogo) {
- Console.WriteLine(CommandLineOptions.Clo.Version);
- }
- if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always) {
- Console.WriteLine("---Command arguments");
- foreach (string arg in args) {
- Contract.Assert(arg != null);
- Console.WriteLine(arg);
- }
-
- Console.WriteLine("--------------------");
- }
-
- Helpers.ExtraTraceInformation("Becoming sentient");
-
- List<string> fileList = new List<string>();
- foreach (string file in CommandLineOptions.Clo.Files) {
- string extension = Path.GetExtension(file);
- if (extension != null) {
- extension = extension.ToLower();
- }
- if (extension == ".txt") {
- StreamReader stream = new StreamReader(file);
- string s = stream.ReadToEnd();
- fileList.AddRange(s.Split(new char[3] {' ', '\n', '\r'}, StringSplitOptions.RemoveEmptyEntries));
- }
- else {
- fileList.Add(file);
- }
- }
- foreach (string file in fileList) {
- Contract.Assert(file != null);
- string extension = Path.GetExtension(file);
- if (extension != null) {
- extension = extension.ToLower();
- }
- if (extension != ".bpl") {
- ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,
- extension == null ? "" : extension);
- goto END;
- }
- }
- ExecutionEngine.ProcessFiles(fileList);
- return 0;
-
- END:
- if (CommandLineOptions.Clo.XmlSink != null) {
- CommandLineOptions.Clo.XmlSink.Close();
- }
- if (CommandLineOptions.Clo.Wait) {
- Console.WriteLine("Press Enter to exit.");
- Console.ReadLine();
- }
- return 1;
- }
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +//--------------------------------------------------------------------------------------------- +// OnlyBoogie OnlyBoogie.ssc +// - main program for taking a BPL program and verifying it +//--------------------------------------------------------------------------------------------- + +namespace Microsoft.Boogie { + using System; + using System.IO; + using System.Collections.Generic; + using System.Diagnostics.Contracts; + + /* + The following assemblies are referenced because they are needed at runtime, not at compile time: + BaseTypes + Provers.Z3 + System.Compiler.Framework + */ + + public class OnlyBoogie + { + + public static int Main(string[] args) + { + Contract.Requires(cce.NonNullElements(args)); + + ExecutionEngine.printer = new ConsolePrinter(); + + CommandLineOptions.Install(new CommandLineOptions()); + + CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; + if (!CommandLineOptions.Clo.Parse(args)) { + goto END; + } + if (CommandLineOptions.Clo.Files.Count == 0) { + ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified."); + goto END; + } + if (CommandLineOptions.Clo.XmlSink != null) { + string errMsg = CommandLineOptions.Clo.XmlSink.Open(); + if (errMsg != null) { + ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg); + goto END; + } + } + if (!CommandLineOptions.Clo.DontShowLogo) { + Console.WriteLine(CommandLineOptions.Clo.Version); + } + if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always) { + Console.WriteLine("---Command arguments"); + foreach (string arg in args) { + Contract.Assert(arg != null); + Console.WriteLine(arg); + } + + Console.WriteLine("--------------------"); + } + + Helpers.ExtraTraceInformation("Becoming sentient"); + + List<string> fileList = new List<string>(); + foreach (string file in CommandLineOptions.Clo.Files) { + string extension = Path.GetExtension(file); + if (extension != null) { + extension = extension.ToLower(); + } + if (extension == ".txt") { + StreamReader stream = new StreamReader(file); + string s = stream.ReadToEnd(); + fileList.AddRange(s.Split(new char[3] {' ', '\n', '\r'}, StringSplitOptions.RemoveEmptyEntries)); + } + else { + fileList.Add(file); + } + } + foreach (string file in fileList) { + Contract.Assert(file != null); + string extension = Path.GetExtension(file); + if (extension != null) { + extension = extension.ToLower(); + } + if (extension != ".bpl") { + ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file, + extension == null ? "" : extension); + goto END; + } + } + ExecutionEngine.ProcessFiles(fileList); + return 0; + + END: + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.Close(); + } + if (CommandLineOptions.Clo.Wait) { + Console.WriteLine("Press Enter to exit."); + Console.ReadLine(); + } + return 1; + } + } +} diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 14d607f9..90e0be41 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -1,324 +1,324 @@ -<?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>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.21022</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <ProjectGuid>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</ProjectGuid>
- <OutputType>Exe</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>BoogieDriver</RootNamespace>
- <AssemblyName>Boogie</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
- <SignAssembly>true</SignAssembly>
- <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>3.5</OldToolsVersion>
- <UpgradeBackupLocation />
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <TargetFrameworkProfile />
- <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>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>TRACE;DEBUG</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly>
- </CodeContractsCustomRewriterAssembly>
- <CodeContractsCustomRewriterClass>
- </CodeContractsCustomRewriterClass>
- <CodeContractsLibPaths>
- </CodeContractsLibPaths>
- <CodeContractsExtraRewriteOptions>
- </CodeContractsExtraRewriteOptions>
- <CodeContractsExtraAnalysisOptions>
- </CodeContractsExtraAnalysisOptions>
- <CodeContractsBaseLineFile>
- </CodeContractsBaseLineFile>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisRuleAssemblies>
- </CodeAnalysisRuleAssemblies>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for BoogieDriver.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <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>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <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>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\Debug\</OutputPath>
- <DefineConstants>TRACE;DEBUG</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
- <OutputPath>bin\x86\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <Optimize>true</Optimize>
- <DebugType>pdbonly</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>bin\Release\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'z3apidebug|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>bin\z3apidebug\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for BoogieDriver.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>x86</PlatformTarget>
- <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
- <WarningLevel>4</WarningLevel>
- <Optimize>false</Optimize>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\QED\</OutputPath>
- <DefineConstants>TRACE;DEBUG</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|x86'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>TRACE;DEBUG</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Data" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="BoogieDriver.cs" />
- <Compile Include="..\version.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\AbsInt\AbsInt.csproj">
- <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>
- <Name>AbsInt</Name>
- </ProjectReference>
- <ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
- <Name>Basetypes</Name>
- </ProjectReference>
- <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
- <Name>CodeContractsExtender</Name>
- </ProjectReference>
- <ProjectReference Include="..\Core\Core.csproj">
- <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
- <Name>Core</Name>
- </ProjectReference>
- <ProjectReference Include="..\Doomed\Doomed.csproj">
- <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>
- <Name>Doomed</Name>
- </ProjectReference>
- <ProjectReference Include="..\ExecutionEngine\ExecutionEngine.csproj">
- <Project>{EAA5EB79-D475-4601-A59B-825C191CD25F}</Project>
- <Name>ExecutionEngine</Name>
- </ProjectReference>
- <ProjectReference Include="..\Graph\Graph.csproj">
- <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
- <Name>Graph</Name>
- </ProjectReference>
- <ProjectReference Include="..\Houdini\Houdini.csproj">
- <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>
- <Name>Houdini</Name>
- </ProjectReference>
- <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
- <Name>ParserHelper</Name>
- </ProjectReference>
- <ProjectReference Include="..\Predication\Predication.csproj">
- <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project>
- <Name>Predication</Name>
- </ProjectReference>
- <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">
- <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>
- <Name>SMTLib</Name>
- </ProjectReference>
- <ProjectReference Include="..\VCExpr\VCExpr.csproj">
- <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
- <Name>VCExpr</Name>
- </ProjectReference>
- <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
- <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
- <Name>VCGeneration</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Folder Include="Properties\" />
- </ItemGroup>
- <ItemGroup>
- <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>true</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.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
+<?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> + <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform> + <ProductVersion>9.0.21022</ProductVersion> + <SchemaVersion>2.0</SchemaVersion> + <ProjectGuid>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</ProjectGuid> + <OutputType>Exe</OutputType> + <AppDesignerFolder>Properties</AppDesignerFolder> + <RootNamespace>BoogieDriver</RootNamespace> + <AssemblyName>Boogie</AssemblyName> + <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> + <FileAlignment>512</FileAlignment> + <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> + <SignAssembly>true</SignAssembly> + <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile> + <FileUpgradeFlags> + </FileUpgradeFlags> + <OldToolsVersion>3.5</OldToolsVersion> + <UpgradeBackupLocation /> + <IsWebBootstrapper>false</IsWebBootstrapper> + <TargetFrameworkProfile /> + <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> + <UseApplicationTrust>false</UseApplicationTrust> + <BootstrapperEnabled>true</BootstrapperEnabled> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> + <DebugSymbols>true</DebugSymbols> + <DebugType>full</DebugType> + <Optimize>false</Optimize> + <OutputPath>..\..\Binaries\</OutputPath> + <DefineConstants>TRACE;DEBUG</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking> + <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> + <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> + <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> + <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> + <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations> + <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations> + <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations> + <CodeContractsPointerObligations>False</CodeContractsPointerObligations> + <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis> + <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions> + <CodeContractsRunInBackground>True</CodeContractsRunInBackground> + <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies> + <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> + <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> + <CodeContractsCustomRewriterAssembly> + </CodeContractsCustomRewriterAssembly> + <CodeContractsCustomRewriterClass> + </CodeContractsCustomRewriterClass> + <CodeContractsLibPaths> + </CodeContractsLibPaths> + <CodeContractsExtraRewriteOptions> + </CodeContractsExtraRewriteOptions> + <CodeContractsExtraAnalysisOptions> + </CodeContractsExtraAnalysisOptions> + <CodeContractsBaseLineFile> + </CodeContractsBaseLineFile> + <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> + <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' "> + <DebugType>pdbonly</DebugType> + <Optimize>true</Optimize> + <OutputPath>..\..\Binaries\</OutputPath> + <DefineConstants>TRACE</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' "> + <DebugSymbols>true</DebugSymbols> + <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>x86</PlatformTarget> + <CodeAnalysisRuleAssemblies> + </CodeAnalysisRuleAssemblies> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>Migrated rules for BoogieDriver.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules> + <WarningLevel>4</WarningLevel> + <Optimize>false</Optimize> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>..\..\Binaries\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>AnyCPU</PlatformTarget> + <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> + <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> + <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> + <CodeContractsPointerObligations>False</CodeContractsPointerObligations> + <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> + <WarningLevel>4</WarningLevel> + <Optimize>false</Optimize> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>bin\x86\Debug\</OutputPath> + <DefineConstants>TRACE;DEBUG</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>x86</PlatformTarget> + <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> + <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets> + <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> + <WarningLevel>4</WarningLevel> + <Optimize>false</Optimize> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'"> + <OutputPath>bin\x86\Release\</OutputPath> + <DefineConstants>TRACE</DefineConstants> + <Optimize>true</Optimize> + <DebugType>pdbonly</DebugType> + <PlatformTarget>x86</PlatformTarget> + <CodeAnalysisLogFile>bin\Release\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> + <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets> + <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> + <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules> + <WarningLevel>4</WarningLevel> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'z3apidebug|x86'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>bin\x86\z3apidebug\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>x86</PlatformTarget> + <CodeAnalysisLogFile>bin\z3apidebug\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>Migrated rules for BoogieDriver.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> + <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets> + <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules> + <WarningLevel>4</WarningLevel> + <Optimize>false</Optimize> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>bin\x86\Checked\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>x86</PlatformTarget> + <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> + <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets> + <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> + <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules> + <WarningLevel>4</WarningLevel> + <Optimize>false</Optimize> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>bin\QED\</OutputPath> + <DefineConstants>TRACE;DEBUG</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>AnyCPU</PlatformTarget> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|x86'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>..\..\Binaries\</OutputPath> + <DefineConstants>TRACE;DEBUG</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>AnyCPU</PlatformTarget> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets> + </PropertyGroup> + <ItemGroup> + <Reference Include="System" /> + <Reference Include="System.Data" /> + <Reference Include="System.Xml" /> + </ItemGroup> + <ItemGroup> + <Compile Include="BoogieDriver.cs" /> + <Compile Include="..\version.cs" /> + </ItemGroup> + <ItemGroup> + <ProjectReference Include="..\AbsInt\AbsInt.csproj"> + <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project> + <Name>AbsInt</Name> + </ProjectReference> + <ProjectReference Include="..\Basetypes\Basetypes.csproj"> + <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> + <Name>Basetypes</Name> + </ProjectReference> + <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj"> + <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project> + <Name>CodeContractsExtender</Name> + </ProjectReference> + <ProjectReference Include="..\Core\Core.csproj"> + <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project> + <Name>Core</Name> + </ProjectReference> + <ProjectReference Include="..\Doomed\Doomed.csproj"> + <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project> + <Name>Doomed</Name> + </ProjectReference> + <ProjectReference Include="..\ExecutionEngine\ExecutionEngine.csproj"> + <Project>{EAA5EB79-D475-4601-A59B-825C191CD25F}</Project> + <Name>ExecutionEngine</Name> + </ProjectReference> + <ProjectReference Include="..\Graph\Graph.csproj"> + <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project> + <Name>Graph</Name> + </ProjectReference> + <ProjectReference Include="..\Houdini\Houdini.csproj"> + <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project> + <Name>Houdini</Name> + </ProjectReference> + <ProjectReference Include="..\ParserHelper\ParserHelper.csproj"> + <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project> + <Name>ParserHelper</Name> + </ProjectReference> + <ProjectReference Include="..\Predication\Predication.csproj"> + <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project> + <Name>Predication</Name> + </ProjectReference> + <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj"> + <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project> + <Name>SMTLib</Name> + </ProjectReference> + <ProjectReference Include="..\VCExpr\VCExpr.csproj"> + <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project> + <Name>VCExpr</Name> + </ProjectReference> + <ProjectReference Include="..\VCGeneration\VCGeneration.csproj"> + <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project> + <Name>VCGeneration</Name> + </ProjectReference> + </ItemGroup> + <ItemGroup> + <Folder Include="Properties\" /> + </ItemGroup> + <ItemGroup> + <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>true</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. + <Target Name="BeforeBuild"> + </Target> + <Target Name="AfterBuild"> + </Target> + --> </Project>
\ No newline at end of file diff --git a/Source/BoogieDriver/cce.cs b/Source/BoogieDriver/cce.cs index 23d79815..42cabfcb 100644 --- a/Source/BoogieDriver/cce.cs +++ b/Source/BoogieDriver/cce.cs @@ -1,105 +1,105 @@ -
-using System;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-using Microsoft.Boogie;
-
- /// <summary>
- /// A class containing static methods to extend the functionality of Code Contracts
- /// </summary>
-
-public static class cce {
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
- return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values);
- }
- [Pure]
- public static bool NonNullElements(VariableSeq collection) {
- return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
- }
- [Pure]
- public static void BeginExpose(object o) {
- }
- [Pure]
- public static void EndExpose() {
- }
- [Pure]
- public static bool IsPeerConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposable(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposed(object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- [Pure]
- public static void AssignSame(object o, object p) {
- }
- [Pure]
- public static object ElementProxy(object o) {
- return o;
- }
- [Pure]
- public static bool None(object o) {
- return true;
- }
- }
- [Pure]
- public static void LoopInvariant(bool p) {
- Contract.Assert(p);
- }
-
- public class UnreachableException : Exception {
- public UnreachableException() {
- }
- }
-}
-
-public class PeerAttribute : System.Attribute {
-}
-public class RepAttribute : System.Attribute {
-}
-public class CapturedAttribute : System.Attribute {
-}
-public class NotDelayedAttribute : System.Attribute {
-}
-public class NoDefaultContractAttribute : System.Attribute {
-}
-public class VerifyAttribute : System.Attribute {
- public VerifyAttribute(bool b) {
-
- }
-}
-public class StrictReadonlyAttribute : System.Attribute {
- }
-public class AdditiveAttribute : System.Attribute {
-}
-public class ReadsAttribute : System.Attribute {
- public enum Reads {
- Nothing,
- };
- public ReadsAttribute(object o) {
- }
-}
+ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +using Microsoft.Boogie; + + /// <summary> + /// A class containing static methods to extend the functionality of Code Contracts + /// </summary> + +public static class cce { + [Pure] + public static T NonNull<T>(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements<T>(IEnumerable<T> collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) { + return collection != null && NonNullElements(collection.Keys) && NonNullElements(collection.Values); + } + [Pure] + public static bool NonNullElements(VariableSeq collection) { + return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + } + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + + public class UnreachableException : Exception { + public UnreachableException() { + } + } +} + +public class PeerAttribute : System.Attribute { +} +public class RepAttribute : System.Attribute { +} +public class CapturedAttribute : System.Attribute { +} +public class NotDelayedAttribute : System.Attribute { +} +public class NoDefaultContractAttribute : System.Attribute { +} +public class VerifyAttribute : System.Attribute { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : System.Attribute { + } +public class AdditiveAttribute : System.Attribute { +} +public class ReadsAttribute : System.Attribute { + public enum Reads { + Nothing, + }; + public ReadsAttribute(object o) { + } +} |