11 files changed, 1884 insertions, 0 deletions

diff --git a/BCT/BCT.sln b/BCT/BCT.sln
new file mode 100644
index 00000000..88a85272
--- /dev/null
+++ b/BCT/BCT.sln
@@ -0,0 +1,166 @@
+

+Microsoft Visual Studio Solution File, Format Version 10.00

+# Visual Studio 2008

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BytecodeTranslator", "BytecodeTranslator\BytecodeTranslator.csproj", "{9C8E4D74-0251-479D-ADAC-A9A469977301}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeModel", "..\..\Felt\SourceObjectModel\CodeModel.csproj", "{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILToCodeModel", "..\..\Felt\ILToCodeModel\ILToCodeModel.csproj", "{27F2A417-B6ED-43AD-A38E-A0B6142216F6}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "MetadataHelper", "..\..\Felt\ObjectModelHelper\MetadataHelper.csproj", "{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "MetadataModel", "..\..\Felt\ObjectModel\MetadataModel.csproj", "{33CAB640-0D03-43DF-81BD-22CDC6C0A597}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "MutableCodeModel", "..\..\Felt\MutableObjectModel\MutableCodeModel.csproj", "{319E150C-8F33-49E7-81CA-30F02F9BA90A}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "MutableMetadataModel", "..\..\Felt\MutableMetadataModel\MutableMetadataModel.csproj", "{319E151C-8F33-49E7-81C9-30F02F9BA90A}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "PdbReader", "..\..\Felt\PdbReader\PdbReader.csproj", "{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "PeReader", "..\..\Felt\ModuleReadWrite\ModuleReadWrite\PeReader.csproj", "{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SourceModel", "..\..\Felt\SourceModel\SourceModel.csproj", "{4B0054FD-124A-4037-9965-BDB55E6BF389}"

+EndProject

+Global

+	GlobalSection(TeamFoundationVersionControl) = preSolution

+		SccNumberOfProjects = 9

+		SccEnterpriseProvider = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccTeamFoundationServer = http://vstfdevdiv:8080/

+		SccProjectUniqueName0 = ..\\..\\Felt\\SourceObjectModel\\CodeModel.csproj

+		SccProjectName0 = $/FELT/SourceObjectModel

+		SccAuxPath0 = http://vstfdevdiv:8080

+		SccLocalPath0 = ..\\..\\Felt\\SourceObjectModel

+		SccProvider0 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName1 = ..\\..\\Felt\\ILToCodeModel\\ILToCodeModel.csproj

+		SccProjectName1 = $/FELT/ILToCodeModel

+		SccAuxPath1 = http://vstfdevdiv:8080

+		SccLocalPath1 = ..\\..\\Felt\\ILToCodeModel

+		SccProvider1 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName2 = ..\\..\\Felt\\ObjectModelHelper\\MetadataHelper.csproj

+		SccProjectName2 = $/FELT/ObjectModelHelper

+		SccAuxPath2 = http://vstfdevdiv:8080

+		SccLocalPath2 = ..\\..\\Felt\\ObjectModelHelper

+		SccProvider2 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName3 = ..\\..\\Felt\\ObjectModel\\MetadataModel.csproj

+		SccProjectName3 = $/FELT/ObjectModel

+		SccAuxPath3 = http://vstfdevdiv:8080

+		SccLocalPath3 = ..\\..\\Felt\\ObjectModel

+		SccProvider3 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName4 = ..\\..\\Felt\\MutableObjectModel\\MutableCodeModel.csproj

+		SccProjectName4 = $/FELT/MutableObjectModel

+		SccAuxPath4 = http://vstfdevdiv:8080

+		SccLocalPath4 = ..\\..\\Felt\\MutableObjectModel

+		SccProvider4 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName5 = ..\\..\\Felt\\MutableMetadataModel\\MutableMetadataModel.csproj

+		SccProjectName5 = $/FELT/MutableMetadataModel

+		SccAuxPath5 = http://vstfdevdiv:8080

+		SccLocalPath5 = ..\\..\\Felt\\MutableMetadataModel

+		SccProvider5 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName6 = ..\\..\\Felt\\PdbReader\\PdbReader.csproj

+		SccProjectName6 = $/FELT/PdbReader

+		SccAuxPath6 = http://vstfdevdiv:8080

+		SccLocalPath6 = ..\\..\\Felt\\PdbReader

+		SccProvider6 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName7 = ..\\..\\Felt\\ModuleReadWrite\\ModuleReadWrite\\PeReader.csproj

+		SccProjectName7 = $/FELT/ModuleReadWrite/ModuleReadWrite

+		SccAuxPath7 = http://vstfdevdiv:8080

+		SccLocalPath7 = ..\\..\\Felt\\ModuleReadWrite\\ModuleReadWrite

+		SccProvider7 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+		SccProjectUniqueName8 = ..\\..\\Felt\\SourceModel\\SourceModel.csproj

+		SccProjectName8 = $/FELT/SourceModel

+		SccAuxPath8 = http://vstfdevdiv:8080

+		SccLocalPath8 = ..\\..\\Felt\\SourceModel

+		SccProvider8 = {4CA58AB2-18FA-4F8D-95D4-32DDF27D184C}

+	EndGlobalSection

+	GlobalSection(SolutionConfigurationPlatforms) = preSolution

+		Debug|Any CPU = Debug|Any CPU

+		NightlyDebug|Any CPU = NightlyDebug|Any CPU

+		NightlyRelease|Any CPU = NightlyRelease|Any CPU

+		Release|Any CPU = Release|Any CPU

+	EndGlobalSection

+	GlobalSection(ProjectConfigurationPlatforms) = postSolution

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{9C8E4D74-0251-479D-ADAC-A9A469977301}.Release|Any CPU.Build.0 = Release|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}.Release|Any CPU.Build.0 = Release|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{27F2A417-B6ED-43AD-A38E-A0B6142216F6}.Release|Any CPU.Build.0 = Release|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.NightlyDebug|Any CPU.ActiveCfg = NightlyDebug|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.NightlyDebug|Any CPU.Build.0 = NightlyDebug|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.NightlyRelease|Any CPU.ActiveCfg = NightlyRelease|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.NightlyRelease|Any CPU.Build.0 = NightlyRelease|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}.Release|Any CPU.Build.0 = Release|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.NightlyDebug|Any CPU.ActiveCfg = NightlyDebug|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.NightlyDebug|Any CPU.Build.0 = NightlyDebug|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.NightlyRelease|Any CPU.ActiveCfg = NightlyRelease|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.NightlyRelease|Any CPU.Build.0 = NightlyRelease|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{33CAB640-0D03-43DF-81BD-22CDC6C0A597}.Release|Any CPU.Build.0 = Release|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.NightlyDebug|Any CPU.ActiveCfg = NightlyDebug|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.NightlyDebug|Any CPU.Build.0 = NightlyDebug|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.NightlyRelease|Any CPU.ActiveCfg = NightlyRelease|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.NightlyRelease|Any CPU.Build.0 = NightlyRelease|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{319E150C-8F33-49E7-81CA-30F02F9BA90A}.Release|Any CPU.Build.0 = Release|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.NightlyDebug|Any CPU.ActiveCfg = NightlyDebug|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.NightlyDebug|Any CPU.Build.0 = NightlyDebug|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.NightlyRelease|Any CPU.ActiveCfg = NightlyRelease|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.NightlyRelease|Any CPU.Build.0 = NightlyRelease|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{319E151C-8F33-49E7-81C9-30F02F9BA90A}.Release|Any CPU.Build.0 = Release|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}.Release|Any CPU.Build.0 = Release|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.NightlyDebug|Any CPU.ActiveCfg = NightlyDebug|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.NightlyDebug|Any CPU.Build.0 = NightlyDebug|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.NightlyRelease|Any CPU.ActiveCfg = NightlyRelease|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.NightlyRelease|Any CPU.Build.0 = NightlyRelease|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}.Release|Any CPU.Build.0 = Release|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{4B0054FD-124A-4037-9965-BDB55E6BF389}.Release|Any CPU.Build.0 = Release|Any CPU

+	EndGlobalSection

+	GlobalSection(SolutionProperties) = preSolution

+		HideSolutionNode = FALSE

+	EndGlobalSection

+EndGlobal

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
new file mode 100644
index 00000000..69c8e077
--- /dev/null
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -0,0 +1,150 @@
+<?xml version="1.0" encoding="utf-8"?>

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

+  <PropertyGroup>

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

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProductVersion>9.0.30729</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{9C8E4D74-0251-479D-ADAC-A9A469977301}</ProjectGuid>

+    <OutputType>Exe</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>BytecodeTranslator</RootNamespace>

+    <AssemblyName>BytecodeTranslator</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

+    <CodeContractsCustomRewriterAssembly>

+    </CodeContractsCustomRewriterAssembly>

+    <CodeContractsCustomRewriterClass>

+    </CodeContractsCustomRewriterClass>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>False</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsBuildReferenceAssembly>False</CodeContractsBuildReferenceAssembly>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsLibPaths>

+    </CodeContractsLibPaths>

+    <CodeContractsPlatformPath>

+    </CodeContractsPlatformPath>

+    <CodeContractsExtraAnalysisOptions>

+    </CodeContractsExtraAnalysisOptions>

+    <CodeContractsBaseLineFile>

+    </CodeContractsBaseLineFile>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+  </PropertyGroup>

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

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="AbsInt, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\Imported\Boogie\AbsInt.dll</HintPath>

+    </Reference>

+    <Reference Include="AIFramework, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\Imported\Boogie\AIFramework.dll</HintPath>

+    </Reference>

+    <Reference Include="Basetypes, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\Imported\Boogie\Basetypes.dll</HintPath>

+    </Reference>

+    <Reference Include="Core, Version=1.0.21125.0, Culture=neutral, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\Imported\Boogie\Core.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Core">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+    <Reference Include="System.Xml.Linq">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+    <Reference Include="System.Data.DataSetExtensions">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="ExpressionTraverser.cs" />

+    <Compile Include="ClassTraverser.cs" />

+    <Compile Include="MethodTraverser.cs" />

+    <Compile Include="StatementTraverser.cs" />

+    <Compile Include="Program.cs" />

+    <Compile Include="ToplevelTraverser.cs" />

+    <Compile Include="TranslationException.cs" />

+    <Compile Include="TranslationHelper.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <Content Include="Readme.txt" />

+  </ItemGroup>

+  <ItemGroup>

+    <ProjectReference Include="..\..\..\Felt\ILToCodeModel\ILToCodeModel.csproj">

+      <Project>{27F2A417-B6ED-43AD-A38E-A0B6142216F6}</Project>

+      <Name>ILToCodeModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\ModuleReadWrite\ModuleReadWrite\PeReader.csproj">

+      <Project>{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}</Project>

+      <Name>PeReader</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\MutableMetadataModel\MutableMetadataModel.csproj">

+      <Project>{319E151C-8F33-49E7-81C9-30F02F9BA90A}</Project>

+      <Name>MutableMetadataModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\MutableObjectModel\MutableCodeModel.csproj">

+      <Project>{319E150C-8F33-49E7-81CA-30F02F9BA90A}</Project>

+      <Name>MutableCodeModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\ObjectModelHelper\MetadataHelper.csproj">

+      <Project>{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}</Project>

+      <Name>MetadataHelper</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\ObjectModel\MetadataModel.csproj">

+      <Project>{33CAB640-0D03-43DF-81BD-22CDC6C0A597}</Project>

+      <Name>MetadataModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\PdbReader\PdbReader.csproj">

+      <Project>{A6A31B03-7C3D-4DE6-AA73-BE88116BC40A}</Project>

+      <Name>PdbReader</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\SourceModel\SourceModel.csproj">

+      <Project>{4B0054FD-124A-4037-9965-BDB55E6BF389}</Project>

+      <Name>SourceModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\Felt\SourceObjectModel\CodeModel.csproj">

+      <Project>{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}</Project>

+      <Name>CodeModel</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

+    <Folder Include="Properties\" />

+  </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/BCT/BytecodeTranslator/ClassTraverser.cs b/BCT/BytecodeTranslator/ClassTraverser.cs
new file mode 100644
index 00000000..67232f83
--- /dev/null
+++ b/BCT/BytecodeTranslator/ClassTraverser.cs
@@ -0,0 +1,79 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+using Bpl = Microsoft.Boogie;

+

+namespace BytecodeTranslator {

+  /// <summary>

+  /// 

+  /// </summary>

+  internal class ClassTraverser : BaseCodeAndContractTraverser {

+    public readonly ToplevelTraverser ToplevelTraverser;

+

+    private Dictionary<IFieldDefinition, Bpl.GlobalVariable> fieldVarMap = new Dictionary<IFieldDefinition, Microsoft.Boogie.GlobalVariable>();

+

+    private Dictionary<IMethodDefinition, MethodTraverser> methodMap = new Dictionary<IMethodDefinition, MethodTraverser>();

+

+    // TODO: (mschaef) just a stub

+    public readonly Bpl.Variable ThisVariable = TranslationHelper.TempThisVar();

+

+    public readonly Bpl.Variable HeapVariable = TranslationHelper.TempHeapVar();

+

+    public ClassTraverser(IContractProvider cp, ToplevelTraverser tlTraverser)

+      : base(cp) {

+      ToplevelTraverser = tlTraverser;

+    }

+

+    public Bpl.Variable FindOrCreateFieldVariable(IFieldDefinition field) {

+      Bpl.GlobalVariable v;

+      if (!fieldVarMap.TryGetValue(field, out v)) {

+        string fieldname = field.ContainingTypeDefinition.ToString() + "." + field.Name.Value;

+        Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(field.Locations);

+        Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);

+        Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);

+

+        v = new Bpl.GlobalVariable(tok,tident);

+        fieldVarMap.Add(field, v);

+        ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Constant(tok, tident, true));

+      }

+      return v;

+    }

+

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="method"></param>

+    public override void Visit(IMethodDefinition method) {

+      // check if it's static and so on

+      MethodTraverser mt;

+      if (!methodMap.TryGetValue(method, out mt)) {

+        mt = new MethodTraverser(this.contractProvider, this);

+      }

+      mt.Visit(method);

+    }

+

+    public override void Visit(IFieldDefinition fieldDefinition) {

+      this.FindOrCreateFieldVariable(fieldDefinition);

+    }

+

+    public override void Visit(ITypeInvariant typeInvariant) {

+      // Todo: Not implemented

+      base.Visit(typeInvariant);

+    }

+

+  }

+}

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
new file mode 100644
index 00000000..2db2e403
--- /dev/null
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -0,0 +1,565 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+using Bpl = Microsoft.Boogie;

+

+

+namespace BytecodeTranslator {

+  class ExpressionTraverser : BaseCodeTraverser {

+

+    // warning! this has to be replaced by a HeapVariable from outside

+    public readonly Bpl.Variable HeapVariable;        

+

+    public readonly StatementTraverser StmtTraverser;

+

+    public readonly Stack<Bpl.Expr> TranslatedExpressions;

+

+    #region Constructors

+

+    public ExpressionTraverser(StatementTraverser stmtTraverser) {

+      HeapVariable = stmtTraverser.HeapVariable;

+      StmtTraverser = stmtTraverser;

+      TranslatedExpressions = new Stack<Bpl.Expr>();

+    }

+

+    public ExpressionTraverser(ClassTraverser classTraverser) {

+      // TODO

+      //StmtTraverser = new StatementTraverser(classTraverser);

+      HeapVariable = classTraverser.HeapVariable;

+      TranslatedExpressions = new Stack<Bpl.Expr>();

+    }

+

+    public ExpressionTraverser(MethodTraverser methodTraverser) {

+      HeapVariable = methodTraverser.HeapVariable;

+      StmtTraverser = new StatementTraverser(methodTraverser);

+      TranslatedExpressions = new Stack<Bpl.Expr>();

+    }

+

+    public ExpressionTraverser(StatementTraverser stmtTraverser, Bpl.Variable heapvar) {

+      HeapVariable = heapvar;

+      StmtTraverser = stmtTraverser;

+      TranslatedExpressions = new Stack<Bpl.Expr>();

+    }

+

+    public ExpressionTraverser(ClassTraverser classTraverser, Bpl.Variable heapvar) {

+      HeapVariable = heapvar;

+      // TODO

+      //StmtTraverser = new StatementTraverser(classTraverser);

+      TranslatedExpressions = new Stack<Bpl.Expr>();

+    }

+

+    public ExpressionTraverser(MethodTraverser methodTraverser, Bpl.Variable heapvar) {

+      HeapVariable = heapvar;

+      StmtTraverser = new StatementTraverser(methodTraverser);

+      TranslatedExpressions = new Stack<Bpl.Expr>();

+    }

+    #endregion

+

+    #region Translate Variable Access

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="addressableExpression"></param>

+    /// <remarks>still a stub</remarks>

+    public override void Visit(IAddressableExpression addressableExpression) {

+      ILocalDefinition/*?*/ local = addressableExpression.Definition as ILocalDefinition;

+      if (local != null) {

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));

+        return;

+      }

+      IParameterDefinition/*?*/ param = addressableExpression.Definition as IParameterDefinition;

+      if (param != null) {

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));

+        return;

+      }

+      IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;

+      if (field != null) {

+        //TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.ClassTraverser.FindOrCreateFieldVariable(field.ResolvedField)));

+        throw new NotImplementedException();

+      }

+      IArrayIndexer/*?*/ arrayIndexer = addressableExpression.Definition as IArrayIndexer;

+      if (arrayIndexer != null) {

+        this.Visit(arrayIndexer);

+        return;

+      }

+      IAddressDereference/*?*/ addressDereference = addressableExpression.Definition as IAddressDereference;

+      if (addressDereference != null) {

+        this.Visit(addressDereference);

+        return;

+      }

+      IMethodReference/*?*/ method = addressableExpression.Definition as IMethodReference;

+      if (method != null) {

+        Console.WriteLine(MemberHelper.GetMethodSignature(method, NameFormattingOptions.Signature));

+        //TODO

+        throw new NotImplementedException();

+      }

+      Debug.Assert(addressableExpression.Definition is IThisReference);

+    }

+

+    public override void Visit(IAddressDereference addressDereference) {

+      this.Visit(addressDereference.Address);

+      throw new NotImplementedException();

+    }

+

+    public override void Visit(IArrayIndexer arrayIndexer) {

+      this.Visit(arrayIndexer.IndexedObject);

+      this.Visit(arrayIndexer.Indices);

+      //TODO            

+    }

+

+    public override void Visit(ITargetExpression targetExpression) {

+      #region ArrayIndexer

+      IArrayIndexer/*?*/ indexer = targetExpression.Definition as IArrayIndexer;

+      if (indexer != null) {

+        this.Visit(indexer);

+        return;

+      }

+      #endregion

+

+      #region AddressDereference

+      IAddressDereference/*?*/ deref = targetExpression.Definition as IAddressDereference;

+      if (deref != null) {

+        IAddressOf/*?*/ addressOf = deref.Address as IAddressOf;

+        if (addressOf != null) {

+          this.Visit(addressOf.Expression);

+          return;

+        }

+        if (targetExpression.Instance != null) {

+          // TODO

+          throw new NotImplementedException("targetExpr->AddrDeRef->InstanceNull");

+        } else if (deref.Address.Type is IPointerTypeReference)

+          throw new NotImplementedException("targetExpr->AddrDeRef->Pointertype");

+        this.Visit(deref.Address);

+        return;

+      }

+      #endregion

+

+      #region LocalDefinition

+      ILocalDefinition/*?*/ local = targetExpression.Definition as ILocalDefinition;

+      if (local != null) {

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));

+        return;

+      }

+      #endregion

+

+      #region ParameterDefenition

+      IParameterDefinition param = targetExpression.Definition as IParameterDefinition;

+      if (param != null) {

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));

+        return;

+      }

+      #endregion

+

+      #region FieldReference

+      IFieldReference field = targetExpression.Definition as IFieldReference;

+      if (field != null) {

+        ProcessFieldVariable(field, targetExpression.Instance, false);

+        return;

+      }

+      #endregion

+

+      #region PropertyDefiniton

+      IPropertyDefinition prop = targetExpression.Definition as IPropertyDefinition;

+      if (prop != null) {

+        throw new NotImplementedException("targetExpr->Property");

+      }

+      #endregion

+    }

+    

+    public override void Visit(IThisReference thisReference) {

+      TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(thisReference.Locations),

+        this.StmtTraverser.MethodTraverser.ClassTraverser.ThisVariable));

+    }

+

+    public override void Visit(IBoundExpression boundExpression) {

+      //if (boundExpression.Instance != null)

+      //{

+      //    this.Visit(boundExpression.Instance);

+      //    // TODO: (mschaef) look where it's bound and do something

+      //}

+      #region LocalDefinition

+      ILocalDefinition local = boundExpression.Definition as ILocalDefinition;

+      if (local != null) {

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));

+        return;

+      }

+      #endregion

+

+      #region ParameterDefiniton

+      IParameterDefinition param = boundExpression.Definition as IParameterDefinition;

+      if (param != null) {

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));

+        return;

+      }

+      #endregion

+

+      #region FieldDefinition

+      IFieldReference field = boundExpression.Definition as IFieldReference;

+      if (field != null) {

+        if (boundExpression.Instance != null) {

+          ProcessFieldVariable(field, boundExpression.Instance,true);

+          return;

+        } else {

+          throw new NotImplementedException(String.Format("Field {0} with Instance NULL.", boundExpression.ToString()));

+        }

+      }

+      #endregion

+

+      #region PropertyDefinition

+      IPropertyDefinition prop = boundExpression.Definition as IPropertyDefinition;

+      if (prop != null) {

+        throw new NotImplementedException("Properties are not implemented");

+      }

+      #endregion

+

+      #region ArrayIndexer

+      IArrayIndexer/*?*/ indexer = boundExpression.Definition as IArrayIndexer;

+      if (indexer != null) {

+        this.Visit(indexer);

+        return;

+      }

+      #endregion

+

+      #region AddressDereference

+      IAddressDereference/*?*/ deref = boundExpression.Definition as IAddressDereference;

+      if (deref != null) {

+        IAddressOf/*?*/ addressOf = deref.Address as IAddressOf;

+        if (addressOf != null) {

+          this.Visit(addressOf.Expression);

+          return;

+        }

+        if (boundExpression.Instance != null) {

+          // TODO

+          this.Visit(boundExpression.Instance);

+          Console.Write("->");

+        } else if (deref.Address.Type is IPointerTypeReference)

+          Console.Write("*");

+        this.Visit(deref.Address);

+        return;

+      } else {

+        if (boundExpression.Instance != null) {

+          throw new NotImplementedException("Addr DeRef without instance.");

+        }

+      }

+      #endregion

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="addressOf"></param>

+    /// <remarks>Since we are doing Copy-In,Copy-Out for function calls we can ignore it.

+    /// But will this work for the general case?</remarks>

+    public override void Visit(IAddressOf addressOf) {

+      Visit(addressOf.Expression);      

+    }

+    #endregion

+

+    #region Variable Access Helpers

+    private void ProcessFieldVariable(IFieldReference field, IExpression instance, bool buildSelectExpr) {

+

+      //TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.ClassTraverser.FindOrCreateFieldVariable(field.ResolvedField))

+      TranslatedExpressions.Push( Bpl.Expr.Ident( 

+        this.StmtTraverser.MethodTraverser.ClassTraverser.ToplevelTraverser.FindOrCreateClassField(

+        field.ContainingType.ResolvedType, 

+        field.ResolvedField) ) );

+

+      ExpressionTraverser etrav = new ExpressionTraverser(StmtTraverser);

+      etrav.Visit(instance);

+

+      TranslatedExpressions.Push(etrav.TranslatedExpressions.Pop());

+

+      // if the field access is not a targetexpression we build a select expression

+      // otherwise the assignment visitor will build a mapassignment later on

+      if (buildSelectExpr) {

+        List<Bpl.Expr> elist = new List<Bpl.Expr>();

+

+        while (TranslatedExpressions.Count > 0) {

+          elist.Add(TranslatedExpressions.Pop());

+        }

+        TranslatedExpressions.Push(Bpl.Expr.Select(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(field.Locations), HeapVariable), elist));

+      }

+    }

+

+

+    #endregion

+

+    #region Translate Constant Access

+

+    public override void Visit(ICompileTimeConstant constant) {

+      if (constant.Value == null) {

+        // TODO: (mschaef) hack

+        TranslatedExpressions.Push(Bpl.Expr.False);

+      } else if (constant.Value is bool) {

+        TranslatedExpressions.Push(((bool)constant.Value) ? Bpl.Expr.True : Bpl.Expr.False);

+      } else if (constant.Value is string) {

+        throw new NotImplementedException("Strings are not translated");        

+      } else {

+        // TODO: (mschaef) hack

+        TranslatedExpressions.Push(Bpl.Expr.Literal((int)constant.Value));

+      }

+    }

+

+    #endregion

+

+    #region Translate Method Calls

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="methodCall"></param>

+    /// <remarks>Stub, This one really needs comments!</remarks>

+    public override void Visit(IMethodCall methodCall) {

+

+      #region Translate In Parameters

+

+

+      Bpl.ExprSeq inexpr = new Bpl.ExprSeq();

+

+      #region Create the $this argument for the function call

+      ExpressionTraverser thistraverser = new ExpressionTraverser(StmtTraverser);

+      thistraverser.Visit(methodCall.ThisArgument);

+      inexpr.Add(thistraverser.TranslatedExpressions.Pop());

+      #endregion

+

+      Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

+      IEnumerator<IParameterDefinition> penum = methodCall.MethodToCall.ResolvedMethod.Parameters.GetEnumerator();

+      penum.MoveNext();

+      foreach (IExpression exp in methodCall.Arguments) {

+        if (penum.Current == null) {

+          throw new TranslationException("More Arguments than Parameters in functioncall");

+        }

+        ExpressionTraverser etrav = new ExpressionTraverser(this.StmtTraverser);

+        etrav.Visit(exp);

+        Bpl.Expr e = etrav.TranslatedExpressions.Pop();

+        p2eMap.Add(penum.Current, e);

+        if (!penum.Current.IsOut) {

+          inexpr.Add(e);

+        }

+        

+        penum.MoveNext();

+      }

+      #endregion

+

+      Bpl.IToken cloc = TranslationHelper.CciLocationToBoogieToken(methodCall.Locations);

+

+      // meeting a constructor is always something special

+      if (methodCall.MethodToCall.ResolvedMethod.IsConstructor) {

+        // Todo: do something with the constructor call

+      } else {

+        // Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!

+

+        #region Translate Out vars

+        Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();

+

+        foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {

+          if (kvp.Key.IsOut || kvp.Key.IsByReference) {

+            Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;

+            if (iexp == null) {

+              throw new TranslationException("Trying to pass complex expression as out in functioncall");

+            }

+            outvars.Add(iexp);

+          }

+        }

+        #endregion

+

+        if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

+          Bpl.Variable v = this.StmtTraverser.MethodTraverser.CreateFreshLocal(methodCall.Type.ResolvedType);

+          outvars.Add(new Bpl.IdentifierExpr(cloc, v));

+          TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));

+        }

+        string methodname = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall.ResolvedMethod);

+

+        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, methodname, inexpr, outvars));

+        

+      }

+

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <remarks>(mschaef) Works, but still a stub </remarks>

+    /// <param name="assignment"></param>

+    public override void Visit(IAssignment assignment) {

+      ExpressionTraverser sourcetrav = new ExpressionTraverser(this.StmtTraverser);

+      ExpressionTraverser targettrav = new ExpressionTraverser(this.StmtTraverser);

+

+      #region Transform Right Hand Side ...

+      sourcetrav.Visit(assignment.Source);

+      Bpl.Expr sourceexp = sourcetrav.TranslatedExpressions.Pop();

+      #endregion

+

+      #region ... and now Left Hand Side and build the bpl statement

+

+      targettrav.Visit(assignment.Target);

+

+      if (targettrav.TranslatedExpressions.Count == 1) {

+

+        Bpl.Expr targetexp = targettrav.TranslatedExpressions.Pop();

+        Bpl.IdentifierExpr idexp = targetexp as Bpl.IdentifierExpr;

+        if (idexp != null) {

+          StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(TranslationHelper.CciLocationToBoogieToken(assignment.Locations),

+              idexp, sourceexp));

+          return;

+        } else {

+          throw new TranslationException("Trying to create a SimpleAssign with complex/illegal lefthand side");

+        }

+

+      } else if (targettrav.TranslatedExpressions.Count > 1) {

+

+        Bpl.ExprSeq eseq = new Bpl.ExprSeq();

+

+        while (targettrav.TranslatedExpressions.Count > 0) {

+          eseq.Add(targettrav.TranslatedExpressions.Pop());

+        }

+

+        StmtTraverser.StmtBuilder.Add(Bpl.Cmd.MapAssign(TranslationHelper.CciLocationToBoogieToken(assignment.Locations),

+          new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(assignment.Target.Locations),

+            HeapVariable), eseq, sourceexp));

+        return;

+      } else {

+        throw new TranslationException("Trying to create an Assignment but lefthand side cannot be created");

+      }

+

+      #endregion

+

+    }

+

+

+    #endregion

+

+    #region Translate Binary Operators

+

+    public override void Visit(IAddition addition) {

+      base.Visit(addition);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Add, lexp, rexp));

+    }

+

+    public override void Visit(IDivision division) {

+      base.Visit(division);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, rexp));

+    }

+

+    public override void Visit(ISubtraction subtraction) {

+      base.Visit(subtraction);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, lexp, rexp));

+    }

+

+    public override void Visit(IMultiplication multiplication) {

+      base.Visit(multiplication);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Mul, lexp, rexp));

+    }

+

+    public override void Visit(IModulus modulus) {

+      base.Visit(modulus);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Mod, lexp, rexp));

+    }

+

+    public override void Visit(IGreaterThan greaterThan) {

+      base.Visit(greaterThan);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Gt, lexp, rexp));

+    }

+

+    public override void Visit(IGreaterThanOrEqual greaterEqual) {

+      base.Visit(greaterEqual);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Ge, lexp, rexp));

+    }

+

+    public override void Visit(ILessThan lessThan) {

+      base.Visit(lessThan);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Lt, lexp, rexp));

+    }

+

+    public override void Visit(ILessThanOrEqual lessEqual) {

+      base.Visit(lessEqual);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Le, lexp, rexp));

+    }

+

+    public override void Visit(IEquality equal) {

+      base.Visit(equal);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, lexp, rexp));

+    }

+

+    public override void Visit(INotEquality nonEqual) {

+      base.Visit(nonEqual);

+      Bpl.Expr rexp = TranslatedExpressions.Pop();

+      Bpl.Expr lexp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, lexp, rexp));

+    }

+

+    // TODO: (mschaef) AND and OR are not yet implemented

+

+    #endregion

+

+    #region Translate Unary Operators

+

+    public override void Visit(IUnaryNegation unaryNegation) {

+      base.Visit(unaryNegation);

+      Bpl.Expr exp = TranslatedExpressions.Pop();

+      Bpl.Expr zero = Bpl.Expr.Literal(0); // TODO: (mschaef) will this work in any case?

+      TranslatedExpressions.Push( Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, zero, exp) );

+    }

+

+    public override void Visit(ILogicalNot logicalNot) {

+      base.Visit(logicalNot);

+      Bpl.Expr exp = TranslatedExpressions.Pop();

+      TranslatedExpressions.Push(Bpl.Expr.Unary(

+          TranslationHelper.CciLocationToBoogieToken(logicalNot.Locations),

+          Bpl.UnaryOperator.Opcode.Not, exp));

+

+    }

+    #endregion

+

+    #region CodeContract Expressions

+    public override void Visit(IOldValue oldValue) {

+      base.Visit(oldValue);

+      TranslatedExpressions.Push(new Bpl.OldExpr(TranslationHelper.CciLocationToBoogieToken(oldValue.Locations),

+        TranslatedExpressions.Pop()));

+    }

+    

+    public override void Visit(IReturnValue returnValue) {

+      if (this.StmtTraverser.MethodTraverser.RetVariable == null) {

+        throw new TranslationException(String.Format("Don't know what to do with return value {0}", returnValue.ToString()));

+      }

+      TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(returnValue.Locations),

+        this.StmtTraverser.MethodTraverser.RetVariable));

+

+    }

+    #endregion

+  }

+}

diff --git a/BCT/BytecodeTranslator/MethodTraverser.cs b/BCT/BytecodeTranslator/MethodTraverser.cs
new file mode 100644
index 00000000..45cb6b6c
--- /dev/null
+++ b/BCT/BytecodeTranslator/MethodTraverser.cs
@@ -0,0 +1,332 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+using Bpl = Microsoft.Boogie;

+

+namespace BytecodeTranslator {

+  class MethodTraverser : BaseCodeAndContractTraverser {

+    public readonly ClassTraverser ClassTraverser;

+

+    private Bpl.Procedure procedure;

+

+    public Bpl.Variable RetVariable;

+

+    public List<MethodParameter> OutVars = new List<MethodParameter>();

+

+    public Bpl.Variable HeapVariable;        

+

+    private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

+

+    internal class MethodParameter {

+      public MethodParameter() {

+        localParameter = null;

+        inParameterCopy = null;

+        outParameterCopy = null;

+      }

+

+      public Bpl.Formal localParameter;

+      public Bpl.Formal inParameterCopy;

+      public Bpl.Formal outParameterCopy;

+    }

+

+    private Dictionary<IParameterDefinition, MethodParameter> formalMap = new Dictionary<IParameterDefinition, MethodParameter>();

+

+    #region Helper Functions

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="local"></param>

+    /// <returns></returns>

+    public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {

+      Bpl.LocalVariable v;

+      Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(local.Locations);

+      Bpl.Type t = TranslationHelper.CciTypeToBoogie(local.Type.ResolvedType);

+      if (!localVarMap.TryGetValue(local, out v)) {

+        v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));

+        localVarMap.Add(local, v);

+      }

+      return v;

+    }

+

+    /// <summary>

+    /// Creates a fresh local var of the given Type and adds it to the

+    /// Bpl Implementation

+    /// </summary>

+    /// <param name="typedef"> The type of the new variable </param>

+    /// <returns> A fresh Variable with automatic generated name and location </returns>

+    public Bpl.Variable CreateFreshLocal(ITypeDefinition typedef) {

+      Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

+      Bpl.Type t = TranslationHelper.CciTypeToBoogie(typedef);

+      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

+      ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

+      localVarMap.Add(dummy, v);

+      return v;

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="param"></param>

+    /// <remarks> (mschaef) only a stub </remarks>

+    private MethodParameter CreateBoogieParameter(IParameterDefinition param) {

+      MethodParameter mparam = new MethodParameter();

+

+      Bpl.Type ptype = Bpl.Type.Int;

+

+      Bpl.Formal v = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

+          new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),

+              param.Name.Value, ptype), false);

+

+      Bpl.Formal v_in = null;

+      if (!param.IsOut) {

+        v_in = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

+            new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),

+                param.Name.Value + "$in", ptype), true);

+      }

+      Bpl.Formal v_out = null;

+      if (param.IsByReference || param.IsOut) {

+        v_out = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

+            new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),

+                param.Name.Value + "$out", ptype), false);

+      }

+      mparam.localParameter = v;

+      mparam.inParameterCopy = v_in;

+      mparam.outParameterCopy = v_out;

+

+      return mparam;

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="param"></param>

+    /// <remarks>STUB</remarks>

+    /// <returns></returns>

+    public Bpl.Variable FindParameterVariable(IParameterDefinition param) {

+      MethodParameter mp;

+      formalMap.TryGetValue(param, out mp);

+      return mp.localParameter;

+    }

+    #endregion

+

+    public MethodTraverser(IContractProvider cp, ClassTraverser cTraverser)

+      : base(cp) {

+      HeapVariable = cTraverser.HeapVariable;

+      procedure = null;

+      ClassTraverser = cTraverser;

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="method"></param>

+    public override void Visit(IMethodDefinition method) {

+

+      try {

+        #region Create in- and out-parameters

+

+        int in_count = 0;

+        int out_count = 0;

+        MethodParameter mp;

+        foreach (IParameterDefinition formal in method.ResolvedMethod.Parameters) {

+

+          mp = CreateBoogieParameter(formal);

+          if (mp.inParameterCopy != null) in_count++;

+          if (mp.outParameterCopy != null) out_count++;

+          formalMap.Add(formal, mp);

+        }

+

+        #region Look for Returnvalue

+

+        // This is just a hack, should be replaced with something more robust

+        if (method.Type.TypeCode != PrimitiveTypeCode.Void) {

+          Bpl.Type rettype = Bpl.Type.Int;

+          out_count++;

+          RetVariable = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),

+              new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),

+                  "$result", rettype), false);

+        } else {

+          RetVariable = null;

+        }

+

+        #endregion

+

+        #region Create $this parameter

+        in_count++;

+        Bpl.Type selftype = Bpl.Type.Int;

+        Bpl.Formal self = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),

+            new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),

+                "$inst", selftype), true);

+

+        #endregion

+

+        Bpl.Variable[] invars = new Bpl.Formal[in_count];

+        Bpl.Variable[] outvars = new Bpl.Formal[out_count];

+

+        int i = 0;

+        int j = 0;

+

+        #region Add $this parameter as first in parameter

+        invars[i++] = self;

+        #endregion

+

+        foreach (MethodParameter mparam in formalMap.Values) {

+          if (mparam.inParameterCopy != null) {

+            invars[i++] = mparam.inParameterCopy;

+          }

+          if (mparam.outParameterCopy != null) {

+            outvars[j++] = mparam.outParameterCopy;

+            OutVars.Add(mparam);

+          }

+        }

+

+        #region add the returnvalue to out if there is one

+        if (RetVariable != null) outvars[j] = RetVariable;

+        #endregion

+       

+        #endregion

+

+        #region Check The Method Contracts

+        Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();

+        Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();

+        Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();

+

+        IMethodContract contract = contractProvider.GetMethodContractFor(method);

+

+        if (contract != null) {

+          try {

+            foreach (IPrecondition pre in contract.Preconditions) {

+              ExpressionTraverser exptravers = new ExpressionTraverser(this);

+              exptravers.Visit(pre.Condition); // TODO

+              // Todo: Deal with Descriptions

+

+

+              Bpl.Requires req

+                  = new Bpl.Requires(TranslationHelper.CciLocationToBoogieToken(pre.Locations),

+                      true, exptravers.TranslatedExpressions.Pop(), "");

+              boogiePrecondition.Add(req);

+            }

+

+            foreach (IPostcondition post in contract.Postconditions) {

+              ExpressionTraverser exptravers = new ExpressionTraverser(this);

+

+              exptravers.Visit(post.Condition);

+              // Todo: Deal with Descriptions

+

+              Bpl.Ensures ens =

+                  new Bpl.Ensures(TranslationHelper.CciLocationToBoogieToken(post.Locations),

+                      true, exptravers.TranslatedExpressions.Pop(), "");

+              boogiePostcondition.Add(ens);

+            }

+

+            foreach (IAddressableExpression mod in contract.ModifiedVariables) {

+              ExpressionTraverser exptravers = new ExpressionTraverser(this);

+              exptravers.Visit(mod);

+

+              Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

+

+              if (idexp == null) {

+                throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));

+              }

+              boogieModifies.Add(idexp);

+            }

+          } catch (TranslationException te) {

+            throw new NotImplementedException("Cannot Handle Errors in Method Contract: " + te.ToString());

+          } catch {

+            throw;

+          }

+        }

+

+        #endregion

+

+        string MethodName = TranslationHelper.CreateUniqueMethodName(method);

+

+        Bpl.Procedure proc = new Bpl.Procedure(TranslationHelper.CciLocationToBoogieToken(method.Locations),

+            MethodName, // make it unique!

+            new Bpl.TypeVariableSeq(),

+            new Bpl.VariableSeq(invars), // in

+            new Bpl.VariableSeq(outvars), // out

+            boogiePrecondition,

+            boogieModifies,

+            boogiePostcondition);

+

+        ClassTraverser.ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(proc);

+

+        this.procedure = proc;

+

+        if (method.IsAbstract) {

+          throw new NotImplementedException("abstract methods are not yet implemented");

+        }

+

+        StatementTraverser stmtTraverser = new StatementTraverser(this);

+

+        #region Add assignements from In-Params to local-Params

+

+        foreach (MethodParameter mparam in formalMap.Values) {

+          if (mparam.inParameterCopy != null) {

+            Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(method.Locations);

+            stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

+              new Bpl.IdentifierExpr(tok, mparam.localParameter),

+              new Bpl.IdentifierExpr(tok, mparam.inParameterCopy)));

+          }

+        }

+

+        #endregion

+

+        try {

+          method.ResolvedMethod.Body.Dispatch(stmtTraverser);

+        } catch (TranslationException te) {

+          throw new NotImplementedException("No Errorhandling in Mehtodvisitor / " + te.ToString());

+        } catch {

+          throw;

+        }

+

+        #region Create Local Vars For Implementation

+        //Todo: (mschaef) hack, there must be a better way to copy this

+        Bpl.Variable[] vars = new Bpl.Variable[localVarMap.Values.Count + formalMap.Values.Count];

+        i = 0;

+        foreach (Bpl.Variable v in localVarMap.Values) {

+          vars[i++] = v;

+        }

+        foreach (MethodParameter mparam in formalMap.Values) {

+          vars[i++] = mparam.localParameter;

+        }

+

+        Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars);

+        #endregion

+

+        Bpl.Implementation impl =

+            new Bpl.Implementation(TranslationHelper.CciLocationToBoogieToken(method.Locations),

+                MethodName, // make unique

+                new Microsoft.Boogie.TypeVariableSeq(),

+                new Microsoft.Boogie.VariableSeq(invars),

+                new Microsoft.Boogie.VariableSeq(outvars),

+                vseq,

+                stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));

+

+        impl.Proc = proc;

+        ClassTraverser.ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(impl);

+      } catch (TranslationException te) {

+        throw new NotImplementedException(te.ToString());

+      } catch {

+        throw;

+      } finally {

+        // Maybe this is a good place to add the procedure to the toplevel declarations

+      }

+    }

+

+  }

+}

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
new file mode 100644
index 00000000..edb38a9c
--- /dev/null
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -0,0 +1,250 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System;

+using System.IO;

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using System.Collections.Generic;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+namespace BytecodeTranslator {

+  class BCT {

+

+    static int Main(string[] args) {

+

+      int result = 0;

+

+      if (args.Length < 1) {

+        Console.WriteLine("Must specify an input file.");

+        return result;

+      }

+

+      try {

+        result = DoRealWork(args[0]);

+      } catch (Exception e) { // swallow everything and just return an error code

+        Console.WriteLine("Foxtrot failed with uncaught exception: {0}", e.Message);

+        Console.WriteLine("Stack trace: {0}", e.StackTrace);

+        return -1;

+      }

+      return result;

+    }

+

+    static int DoRealWork(string assemblyName) {

+

+      HostEnvironment host = new HostEnvironment();

+      IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;

+      if (module == null || module == Dummy.Module || module == Dummy.Assembly) {

+        Console.WriteLine(assemblyName + " is not a PE file containing a CLR module or assembly, or an error occurred when loading it.");

+        return 1;

+      }

+

+      #region Load any reference assemblies

+      var fileSpec = module.Location;

+      string directory;

+      if (Path.IsPathRooted(fileSpec))

+        directory = Path.GetDirectoryName(fileSpec);

+      else

+        directory = Directory.GetCurrentDirectory();

+      string[] files;

+      Dictionary<string, List<IAssembly>>/*?*/ referenceAssemblies = new Dictionary<string, List<IAssembly>>();

+      #region Look for reference assembly dlls

+      // TODO: Search a user-specified set of paths/directories, not just the one the input came from.

+      files = Directory.GetFiles(directory, "*.Contracts*.dll", SearchOption.TopDirectoryOnly);

+      if (files != null) {

+        foreach (var file in files) {

+          IAssembly/*?*/ refAssem = host.LoadUnitFrom(file) as IAssembly;

+          if (refAssem == null || refAssem == Dummy.Assembly) {

+            Console.WriteLine("Could not load '" + file + "' as a reference assembly.");

+            continue;

+          }

+          var fileName = Path.GetFileNameWithoutExtension(file);

+          var baseName = BCT.NameUpToFirstPeriod(fileName);

+          if (referenceAssemblies.ContainsKey(baseName)) {

+            referenceAssemblies[baseName].Add(refAssem);

+          } else {

+            List<IAssembly> a = new List<IAssembly>();

+            a.Add(refAssem);

+            referenceAssemblies.Add(baseName, a);

+          }

+        }

+      }

+      #endregion Look for reference assembly dlls

+      #endregion Load any reference assemblies

+

+      IAssembly/*?*/ assembly = null;

+

+      PdbReader/*?*/ pdbReader = null;

+      string pdbFile = Path.ChangeExtension(module.Location, "pdb");

+      if (File.Exists(pdbFile)) {

+        Stream pdbStream = File.OpenRead(pdbFile);

+        pdbReader = new PdbReader(pdbStream, host);

+      }

+

+      ContractProvider contractProvider = new ContractProvider(new ContractMethods(host), module);

+      module = ConvertMetadataModelToCodeModel(host, module, pdbReader, contractProvider);

+

+      //SourceToILConverterProvider sourceToILProvider =

+      //  delegate(IMetadataHost host2, ISourceLocationProvider/*?*/ sourceLocationProvider, IContractProvider/*?*/ contractProvider2)

+      //  {

+      //      return new CodeModelToILConverter(host2, sourceLocationProvider, contractProvider2);

+      //  };

+

+

+      List<IAssembly> oobUnits;

+      List<KeyValuePair<IContractProvider, IMetadataHost>> oobProvidersAndHosts = new List<KeyValuePair<IContractProvider, IMetadataHost>>();

+      if (referenceAssemblies.TryGetValue(module.Name.Value, out oobUnits)) {

+        foreach (var oob in oobUnits) {

+          LazyContractProvider ocp = new LazyContractProvider(host, oob, contractProvider.ContractMethods);

+          oobProvidersAndHosts.Add(new KeyValuePair<IContractProvider, IMetadataHost>(ocp, host));

+        }

+      }

+

+      AggregatingContractProvider acp = new AggregatingContractProvider(host, contractProvider, oobProvidersAndHosts);

+

+      #region Pass 3: Translate the code model to BPL

+      //tmp_BPLGenerator translator = new tmp_BPLGenerator(host, acp);

+      ToplevelTraverser translator = new ToplevelTraverser(acp);

+      assembly = module as IAssembly;

+      if (assembly != null)

+        translator.Visit(assembly);

+      else

+        translator.Visit(module);

+      #endregion Pass 3: Translate the code model to BPL

+      Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter("\\lala.txt");

+      translator.TranslatedProgram.Emit(writer);

+      writer.WriteLine(";ENDE");

+      writer.Close();

+      return 0; // success

+    }

+

+    private static string NameUpToFirstPeriod(string name) {

+      var i = name.IndexOf('.');

+      if (i == -1)

+        return name;

+      else

+        return name.Substring(0, i);

+    }

+

+    /// <summary>

+    /// Takes a module which is presumably a metadata model (either immutable or mutable) and returns

+    /// the "same" module which is now a code model module.

+    /// 

+    /// Currently there is no way to lazily convert a module from the metadata model to the code model.

+    /// Therefore, this method works eagerly by visiting the entire <paramref name="module"/>.

+    /// </summary>

+    /// <param name="host">

+    /// The host that was used to load the module.

+    /// </param>

+    /// <param name="module">

+    /// The module which is to be converted.

+    /// </param>

+    /// <param name="pdbReader">

+    /// A PDB reader that is used by ILToCodeModel during the conversion.

+    /// </param>

+    /// <param name="contractProvider">

+    /// A contract provider that is used by ILToCodeModel during the conversion. As part of the conversion, the

+    /// contract provider will become populated with any contracts found during decompilation.

+    /// </param>

+    /// <returns>

+    /// A module that is at the code model level.

+    /// </returns>

+    public static IModule ConvertMetadataModelToCodeModel(IMetadataHost host, IModule module, PdbReader/*?*/ pdbReader, ContractProvider contractProvider) {

+

+      SourceMethodBodyProvider ilToSourceProvider =

+        delegate(IMethodBody methodBody) {

+          return new Microsoft.Cci.ILToCodeModel.SourceMethodBody(methodBody, host, contractProvider, pdbReader);

+        };

+

+      IAssembly/*?*/ assembly;

+

+      #region Just run the code and contract mutator which extracts all contracts to their containing methods

+      CodeAndContractMutator ccm = new CodeAndContractMutator(host, true, ilToSourceProvider, null, pdbReader, contractProvider);

+

+      assembly = module as IAssembly;

+      if (assembly != null)

+        module = ccm.Visit(ccm.GetMutableCopy(assembly));

+      else

+        module = ccm.Visit(ccm.GetMutableCopy(module));

+      #endregion Just run the code and contract mutator which extracts all contracts to their containing methods

+

+      return module;

+    }

+

+  }

+

+  internal class HostEnvironment : MetadataReaderHost {

+    PeReader peReader;

+    internal HostEnvironment()

+      : base(new NameTable(), 4) {

+      this.peReader = new PeReader(this);

+    }

+

+    public override IUnit LoadUnitFrom(string location) {

+      IUnit result = this.peReader.OpenModule(BinaryDocument.GetBinaryDocumentForFile(location, this));

+      this.RegisterAsLatest(result);

+      return result;

+    }

+

+    //public override void ResolvingAssemblyReference(IUnit referringUnit, AssemblyIdentity referencedAssembly) {

+    //  if (referencedAssembly != CoreAssemblySymbolicIdentity) {

+    //    this.LoadAssembly(referencedAssembly);

+    //  }

+    //}

+    private AssemblyIdentity Probe(string probeDir, AssemblyIdentity referencedAssembly) {

+      string path = Path.Combine(probeDir, referencedAssembly.Name.Value + ".dll");

+      if (File.Exists(path)) return new AssemblyIdentity(referencedAssembly, path);

+      return null;

+    }

+    public override AssemblyIdentity ProbeAssemblyReference(IUnit referringUnit, AssemblyIdentity referencedAssembly) {

+      if (string.IsNullOrEmpty(referencedAssembly.Location)) {

+        // probe for in the same directory as the referring unit

+        string probeDir = Path.GetDirectoryName(Path.GetFullPath(referringUnit.Location));

+        AssemblyIdentity result = Probe(probeDir, referencedAssembly);

+        if (result != null) return result;

+        //// Probe in the libPaths directories

+        //foreach (string prefix in this.libPaths) {

+        //  result = Probe(prefix, referencedAssembly);

+        //  if (result != null) return result;

+        //}

+        // Check platform location

+        probeDir = Path.GetDirectoryName(Path.GetFullPath(typeof(object).Assembly.Location));

+        result = Probe(probeDir, referencedAssembly);

+        if (result != null) return result;

+      }

+      return base.ProbeAssemblyReference(referringUnit, referencedAssembly);

+    }

+

+    public override void ResolvingAssemblyReference(IUnit referringUnit, AssemblyIdentity referencedAssembly) {

+      if (string.IsNullOrEmpty(referencedAssembly.Location)) {

+        //base.ResolvingAssemblyReference(referringUnit, referencedAssembly);

+        AssemblyIdentity ai = this.ProbeAssemblyReference(referringUnit, referencedAssembly);

+        if (ai != null && !String.IsNullOrEmpty(ai.Location)) {

+          this.LoadUnit(ai);

+        } else {

+          base.ResolvingAssemblyReference(referringUnit, referencedAssembly);

+        }

+      } else {

+        // REVIEW: Why wasn't LoadUnit called here instead?

+        var location = referencedAssembly.Location;

+        string s = location;

+        if (location.StartsWith("file://")) { // then it is a uri

+          try {

+            Uri u = new Uri(location, UriKind.RelativeOrAbsolute); // construct a URI to normalize it

+            s = u.LocalPath;

+          } catch (UriFormatException) {

+          }

+        }

+        IUnit result = this.peReader.OpenModule(BinaryDocument.GetBinaryDocumentForFile(s, this));

+        this.RegisterAsLatest(result);

+      }

+    }

+

+  }

+

+}

diff --git a/BCT/BytecodeTranslator/Readme.txt b/BCT/BytecodeTranslator/Readme.txt
new file mode 100644
index 00000000..09c21ca6
--- /dev/null
+++ b/BCT/BytecodeTranslator/Readme.txt
@@ -0,0 +1,6 @@
+Current Issues:

+

+-	Just moved the assignement translation from statementtraverser to expressiontraverser

+	since it is in fact an expression. need to test it

+	

+-	The ordering of out params in a method call might be wrong // should be correct by now
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
new file mode 100644
index 00000000..8bc11399
--- /dev/null
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -0,0 +1,175 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+using Bpl = Microsoft.Boogie;

+

+

+namespace BytecodeTranslator

+{

+  internal class StatementTraverser : BaseCodeTraverser {

+    public readonly MethodTraverser MethodTraverser;

+

+    public readonly Bpl.Variable HeapVariable;

+

+    public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();

+

+    #region Constructors

+    public StatementTraverser(MethodTraverser mt) {

+      HeapVariable = mt.HeapVariable;

+      MethodTraverser = mt;

+    }

+

+    public StatementTraverser(MethodTraverser mt, Bpl.Variable heapvar) {

+      HeapVariable = heapvar;

+      MethodTraverser = mt;

+    }

+    #endregion

+

+    public override void Visit(IBlockStatement block) {

+      BasicBlock b = (BasicBlock)block;

+      this.Visit(b);

+    }

+

+    #region Basic Statements

+    /// <summary>

+    /// Visit all statements in a single block

+    /// </summary>

+    /// <param name="b"></param>

+    private void Visit(BasicBlock b) {

+      Bpl.StmtListBuilder slb = new Bpl.StmtListBuilder();

+

+      foreach (IStatement st in b.Statements) {

+        this.Visit(st);

+      }

+    }

+

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <remarks>(mschaef) Works, but still a stub</remarks>

+    /// <param name="conditionalStatement"></param>

+    public override void Visit(IConditionalStatement conditionalStatement) {

+      StatementTraverser thenTraverser = new StatementTraverser(this.MethodTraverser);

+      StatementTraverser elseTraverser = new StatementTraverser(this.MethodTraverser);

+

+      ExpressionTraverser condTraverser = new ExpressionTraverser(this);

+      condTraverser.Visit(conditionalStatement.Condition);

+      thenTraverser.Visit(conditionalStatement.TrueBranch);

+      elseTraverser.Visit(conditionalStatement.FalseBranch);

+

+      Bpl.IfCmd ifcmd = new Bpl.IfCmd(TranslationHelper.CciLocationToBoogieToken(conditionalStatement.Locations),

+          condTraverser.TranslatedExpressions.Pop(),

+          thenTraverser.StmtBuilder.Collect(TranslationHelper.CciLocationToBoogieToken(conditionalStatement.TrueBranch.Locations)),

+          null,

+          elseTraverser.StmtBuilder.Collect(TranslationHelper.CciLocationToBoogieToken(conditionalStatement.FalseBranch.Locations))

+          );

+

+      StmtBuilder.Add(ifcmd);

+

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="expressionStatement"></param>

+    /// <remarks> TODO: might be wrong for the general case</remarks>

+    public override void Visit(IExpressionStatement expressionStatement) {

+

+      ExpressionTraverser etrav = new ExpressionTraverser(this);

+      etrav.Visit(expressionStatement.Expression);

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <remarks>(mschaef) Not Implemented</remarks>

+    /// <param name="breakStatement"></param>

+    public override void Visit(IBreakStatement breakStatement) {

+      StmtBuilder.Add(new Bpl.BreakCmd(TranslationHelper.CciLocationToBoogieToken(breakStatement.Locations), "I dont know"));

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <remarks>(mschaef) not implemented</remarks>

+    /// <param name="returnStatement"></param>

+    public override void Visit(IReturnStatement returnStatement) {

+      Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(returnStatement.Locations);

+

+      #region Copy values of all out parameters to outvariables

+      foreach (MethodTraverser.MethodParameter mp in MethodTraverser.OutVars) {

+        StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

+          new Bpl.IdentifierExpr(tok, mp.outParameterCopy), new Bpl.IdentifierExpr(tok, mp.localParameter)));

+      }

+      #endregion

+

+      if (returnStatement.Expression != null) {

+        ExpressionTraverser etrav = new ExpressionTraverser(this);

+        etrav.Visit(returnStatement.Expression);

+

+        if (this.MethodTraverser.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {

+          throw new TranslationException(String.Format("{0} returns a value that is not supported by the function", returnStatement.ToString()));

+        }

+

+        StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

+            new Bpl.IdentifierExpr(tok, this.MethodTraverser.RetVariable), etrav.TranslatedExpressions.Pop()));

+      }

+      StmtBuilder.Add(new Bpl.ReturnCmd(TranslationHelper.CciLocationToBoogieToken(returnStatement.Locations)));

+    }

+    #endregion

+

+    #region Goto and Labels

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <remarks> STUB </remarks>

+    /// <param name="gotoStatement"></param>

+    public override void Visit(IGotoStatement gotoStatement) {

+      String[] target = new String[1];

+      target[0] = gotoStatement.TargetStatement.Label.Value;

+

+      Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(TranslationHelper.CciLocationToBoogieToken(gotoStatement.Locations),

+          new Bpl.StringSeq(target));

+

+      StmtBuilder.Add(gotocmd);

+    }

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <remarks> (mschaef) not sure if there is more work to do</remarks>

+    /// <param name="labeledStatement"></param>

+    public override void Visit(ILabeledStatement labeledStatement) {

+      StmtBuilder.AddLabelCmd(labeledStatement.Label.Value);

+      base.Visit(labeledStatement.Statement);

+    }

+

+    #endregion

+

+    #region Looping Statements

+

+    public override void Visit(IWhileDoStatement whileDoStatement) {

+      throw new NotImplementedException("While Statements are not implemented");

+    }

+

+

+

+    #endregion

+

+  }

+}

diff --git a/BCT/BytecodeTranslator/ToplevelTraverser.cs b/BCT/BytecodeTranslator/ToplevelTraverser.cs
new file mode 100644
index 00000000..9079b5af
--- /dev/null
+++ b/BCT/BytecodeTranslator/ToplevelTraverser.cs
@@ -0,0 +1,78 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+using Bpl = Microsoft.Boogie;

+

+

+namespace BytecodeTranslator {

+    /// <summary>

+    /// 

+    /// </summary>

+  internal class ToplevelTraverser : BaseCodeAndContractTraverser {

+

+    public readonly IContractProvider ContractProvider;

+

+    public readonly Bpl.Program TranslatedProgram;

+

+    private Dictionary<ITypeDefinition, ClassTraverser> classMap = new Dictionary<ITypeDefinition, ClassTraverser>();

+

+    public ToplevelTraverser(IContractProvider cp)

+      : base(cp) {

+      ContractProvider = cp;

+      TranslatedProgram = new Bpl.Program();

+    }

+

+    public Bpl.Variable FindOrCreateClassField(ITypeDefinition classtype, IFieldDefinition field) {

+      ClassTraverser ct;

+      if (!classMap.TryGetValue(classtype, out ct)) {

+        ct = new ClassTraverser(this.ContractProvider, this);

+        classMap.Add(classtype, ct);

+        return ct.FindOrCreateFieldVariable(field);

+      } else {

+        return ct.FindOrCreateFieldVariable(field);

+      }

+    }

+

+

+    /// <summary>

+    /// 

+    /// </summary>

+    /// <param name="typeDefinition"></param>

+    public override void Visit(ITypeDefinition typeDefinition) {

+      if (typeDefinition.IsClass) {

+

+        ClassTraverser ct;

+        if (!classMap.TryGetValue(typeDefinition, out ct)) { 

+          ct = new ClassTraverser(this.contractProvider, this);

+          classMap.Add(typeDefinition, ct);

+        }

+        ct.Visit(typeDefinition);

+      } else {

+        Console.WriteLine("Non-Class {0} was found", typeDefinition);

+        throw new NotImplementedException(String.Format("Non-Class Type {0} is not yet supported.", typeDefinition.ToString()));

+      }

+    }

+

+    public override void Visit(IModule module) {

+      base.Visit(module);

+    }

+

+    public override void Visit(IAssembly assembly) {

+      base.Visit(assembly);

+    }

+

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationException.cs b/BCT/BytecodeTranslator/TranslationException.cs
new file mode 100644
index 00000000..5aac98af
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationException.cs
@@ -0,0 +1,20 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace BytecodeTranslator {

+  class TranslationException : Exception {

+    

+    public TranslationException(string reason) { 

+    

+    }

+

+

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
new file mode 100644
index 00000000..978a9412
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -0,0 +1,63 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+

+using Bpl = Microsoft.Boogie;

+

+

+namespace BytecodeTranslator {

+    /// <summary>

+    /// Class containing several static helper functions to convert

+    /// from Cci to Boogie Methodology

+    /// </summary>

+  class TranslationHelper {

+

+    public static Bpl.IToken CciLocationToBoogieToken(IEnumerable<ILocation> locations) {

+      Bpl.IToken tok = Bpl.Token.NoToken;

+      return tok;

+    }

+

+    public static Bpl.IToken CciLocationToBoogieToken(ILocation location) {

+      Bpl.IToken tok = Bpl.Token.NoToken;

+      return tok;

+    }

+

+    private static int tmpVarCounter = 0;

+    public static string GenerateTempVarName() {

+      return "$tmp" + (tmpVarCounter++).ToString();

+    }

+

+    public static string CreateUniqueMethodName(IMethodDefinition method) {

+      return method.ContainingType.ToString() + "." + method.Name.Value + "$" + method.Type.ResolvedType.ToString();

+    }

+

+    #region Temp Stuff that must be replaced as soon as there is real code to deal with this

+

+    public static Bpl.Type CciTypeToBoogie(ITypeDefinition type) {

+      return Bpl.Type.Int;

+    }

+

+    public static Bpl.Variable TempHeapVar() {

+      return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$heap", Bpl.Type.Int)); 

+    }

+

+    public static Bpl.Variable TempThisVar() {

+      return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$this", Bpl.Type.Int));

+    }

+

+    #endregion

+

+  }

+}