Added the factory pattern so that all traversers are created through factory methods. This is the beginning of allowing plugins to perform methodology-specific translations.

Added a CLR traverser that is meant to encode the CLR semantics. For now it just does one thing: add the assertion that a divisor should not be zero.
Added an MS Test project so that we can use that for regression testing.

21 files changed, 676 insertions, 111 deletions

diff --git a/BCT/BCT.sln b/BCT/BCT.sln
index 6c5702ae..905cc2ea 100644
--- a/BCT/BCT.sln
+++ b/BCT/BCT.sln
@@ -25,6 +25,19 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeModelToIL", "..\..\CCIC
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGenerator", "..\..\CCICodePlex\Ast\Metadata\Sources\ILGenerator\ILGenerator.csproj", "{08156C78-403A-4112-AD81-8646AC51CD2F}"

 EndProject

+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "RegressionTests", "RegressionTests", "{AA77A7CB-972F-4A5C-A16C-3810B448F6EA}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "RegressionTestInput", "RegressionTests\RegressionTestInput\RegressionTestInput.csproj", "{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}"

+EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TranslationTest", "RegressionTests\TranslationTest\TranslationTest.csproj", "{A112AFBA-D6F6-44A4-A683-C3D458A68D84}"

+EndProject

+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Solution Items", "Solution Items", "{45E691A6-BFA4-4545-93AC-EA7290A6B565}"

+	ProjectSection(SolutionItems) = preProject

+		BCT.vsmdi = BCT.vsmdi

+		Local.testsettings = Local.testsettings

+		TraceAndTestImpact.testsettings = TraceAndTestImpact.testsettings

+	EndProjectSection

+EndProject

 Global

 	GlobalSection(TeamFoundationVersionControl) = preSolution

 		SccNumberOfProjects = 9

@@ -76,6 +89,9 @@ Global
 		SccLocalPath8 = ..\\..\\Felt\\SourceModel

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

 	EndGlobalSection

+	GlobalSection(TestCaseManagementSettings) = postSolution

+		CategoryFile = BCT.vsmdi

+	EndGlobalSection

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		CompilerOnly|Any CPU = CompilerOnly|Any CPU

 		Debug|Any CPU = Debug|Any CPU

@@ -204,8 +220,33 @@ Global
 		{08156C78-403A-4112-AD81-8646AC51CD2F}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

 		{08156C78-403A-4112-AD81-8646AC51CD2F}.Release|Any CPU.ActiveCfg = Release|Any CPU

 		{08156C78-403A-4112-AD81-8646AC51CD2F}.Release|Any CPU.Build.0 = Release|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.CompilerOnly|Any CPU.ActiveCfg = Release|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.CompilerOnly|Any CPU.Build.0 = Release|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}.Release|Any CPU.Build.0 = Release|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.CompilerOnly|Any CPU.ActiveCfg = Release|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.CompilerOnly|Any CPU.Build.0 = Release|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84}.Release|Any CPU.Build.0 = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

 	EndGlobalSection

+	GlobalSection(NestedProjects) = preSolution

+		{3D13D2CC-6387-46FA-BDC2-4BEEFC460118} = {AA77A7CB-972F-4A5C-A16C-3810B448F6EA}

+		{A112AFBA-D6F6-44A4-A683-C3D458A68D84} = {AA77A7CB-972F-4A5C-A16C-3810B448F6EA}

+		{45E691A6-BFA4-4545-93AC-EA7290A6B565} = {AA77A7CB-972F-4A5C-A16C-3810B448F6EA}

+	EndGlobalSection

 EndGlobal

diff --git a/BCT/BCT.vsmdi b/BCT/BCT.vsmdi
new file mode 100644
index 00000000..08dd31d7
--- /dev/null
+++ b/BCT/BCT.vsmdi
@@ -0,0 +1,6 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<TestLists xmlns="http://microsoft.com/schemas/VisualStudio/TeamTest/2010">

+  <TestList name="Lists of Tests" id="8c43106b-9dc1-4907-a29f-aa66a61bf5b6">

+    <RunConfiguration id="f898dc7f-7e79-4656-a1cd-5ca50fff2b5d" name="Local" storage="local.testsettings" type="Microsoft.VisualStudio.TestTools.Common.TestRunConfiguration, Microsoft.VisualStudio.QualityTools.Common, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />

+  </TestList>

+</TestLists>
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 60479a27..e566adff 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -108,6 +108,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Prelude.cs" />

     <Compile Include="ExpressionTraverser.cs" />

     <Compile Include="ClassTraverser.cs" />

@@ -117,6 +118,7 @@
     <Compile Include="ToplevelTraverser.cs" />

     <Compile Include="TranslationException.cs" />

     <Compile Include="TranslationHelper.cs" />

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

   </ItemGroup>

   <ItemGroup>

     <Content Include="Readme.txt" />

diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
new file mode 100644
index 00000000..f52b2006
--- /dev/null
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -0,0 +1,52 @@
+//-----------------------------------------------------------------------------

+//

+// 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 {

+

+  public class CLRSemantics : TraverserFactory {

+

+    public override ExpressionTraverser MakeExpressionTraverser(StatementTraverser parent, Bpl.Variable heapVariable) {

+      return new CLRExpressionSemantics(parent, heapVariable);

+    }

+

+    public class CLRExpressionSemantics : ExpressionTraverser {

+

+      public CLRExpressionSemantics(StatementTraverser stmtTraverser, Bpl.Variable heapvar)

+        : base(stmtTraverser, heapvar) { }

+

+      public override void Visit(IDivision division) {

+        this.Visit(division.LeftOperand);

+        this.Visit(division.RightOperand);

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

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

+

+        var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);

+

+        var loc = this.StmtTraverser.MethodTraverser.CreateFreshLocal(division.RightOperand.Type);

+        var locExpr = Bpl.Expr.Ident(loc);

+        var storeLocal = Bpl.Cmd.SimpleAssign(tok, locExpr, rexp);

+        this.StmtTraverser.StmtBuilder.Add(storeLocal);

+

+        var a = new Bpl.AssertCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, locExpr, Bpl.Expr.Literal(0)));

+        this.StmtTraverser.StmtBuilder.Add(a);

+

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

+      }

+    }

+  }

+}
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/ClassTraverser.cs b/BCT/BytecodeTranslator/ClassTraverser.cs
index 67232f83..ce72c9ba 100644
--- a/BCT/BytecodeTranslator/ClassTraverser.cs
+++ b/BCT/BytecodeTranslator/ClassTraverser.cs
@@ -20,7 +20,10 @@ namespace BytecodeTranslator {
   /// <summary>

   /// 

   /// </summary>

-  internal class ClassTraverser : BaseCodeAndContractTraverser {

+  public class ClassTraverser : BaseCodeAndContractTraverser {

+

+    public readonly TraverserFactory factory;

+

     public readonly ToplevelTraverser ToplevelTraverser;

 

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

@@ -32,8 +35,9 @@ namespace BytecodeTranslator {
 

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

 

-    public ClassTraverser(IContractProvider cp, ToplevelTraverser tlTraverser)

+    public ClassTraverser(TraverserFactory factory, IContractProvider cp, ToplevelTraverser tlTraverser)

       : base(cp) {

+      this.factory = factory;

       ToplevelTraverser = tlTraverser;

     }

 

@@ -61,7 +65,8 @@ namespace BytecodeTranslator {
       // check if it's static and so on

       MethodTraverser mt;

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

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

+        mt = this.factory.MakeMethodTraverser(this, this.contractProvider);

+        this.methodMap.Add(method, mt);

       }

       mt.Visit(method);

     }

@@ -76,4 +81,5 @@ namespace BytecodeTranslator {
     }

 

   }

+

 }

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index ba832fa4..beeb5cb1 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -19,7 +19,7 @@ using Bpl = Microsoft.Boogie;
 

 

 namespace BytecodeTranslator {

-  class ExpressionTraverser : BaseCodeTraverser {

+  public class ExpressionTraverser : BaseCodeTraverser {

 

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

     public readonly Bpl.Variable HeapVariable;        

@@ -30,24 +30,9 @@ namespace BytecodeTranslator {
 

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

+      : this(stmtTraverser, stmtTraverser.HeapVariable)

+    { }

 

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

       HeapVariable = heapvar;

@@ -55,18 +40,6 @@ namespace BytecodeTranslator {
       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

@@ -279,10 +252,7 @@ namespace BytecodeTranslator {
         field.ContainingType.ResolvedType, 

         field.ResolvedField) ) );

 

-      ExpressionTraverser etrav = new ExpressionTraverser(StmtTraverser);

-      etrav.Visit(instance);

-

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

+      this.Visit(instance);

 

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

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

@@ -331,9 +301,8 @@ namespace BytecodeTranslator {
       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());

+      this.Visit(methodCall.ThisArgument);

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

       #endregion

 

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

@@ -343,9 +312,9 @@ namespace BytecodeTranslator {
         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();

+        this.Visit(exp);

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

+

         p2eMap.Add(penum.Current, e);

         if (!penum.Current.IsOut) {

           inexpr.Add(e);

@@ -396,48 +365,24 @@ namespace BytecodeTranslator {
     /// <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();

+      this.Visit(assignment.Source);

+      Bpl.Expr sourceexp = this.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());

-        }

+      this.Visit(assignment.Target);

 

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

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

-            HeapVariable), eseq, sourceexp));

+      Bpl.Expr targetexp = this.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 an Assignment but lefthand side cannot be created");

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

       }

 

-      #endregion

-

     }

 

 

@@ -457,10 +402,6 @@ namespace BytecodeTranslator {
       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

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

-

-      var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);

-      var a = new Bpl.AssertCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, rexp, Bpl.Expr.Literal(0)));

-      this.StmtTraverser.StmtBuilder.Add(a);

     }

 

     public override void Visit(ISubtraction subtraction) {

@@ -599,4 +540,5 @@ namespace BytecodeTranslator {
     }

     #endregion

   }

+

 }

diff --git a/BCT/BytecodeTranslator/MethodTraverser.cs b/BCT/BytecodeTranslator/MethodTraverser.cs
index fdda674d..7a7170e9 100644
--- a/BCT/BytecodeTranslator/MethodTraverser.cs
+++ b/BCT/BytecodeTranslator/MethodTraverser.cs
@@ -17,7 +17,10 @@ using Microsoft.Cci.ILToCodeModel;
 using Bpl = Microsoft.Boogie;

 

 namespace BytecodeTranslator {

-  class MethodTraverser : BaseCodeAndContractTraverser {

+  public class MethodTraverser : BaseCodeAndContractTraverser {

+

+    public readonly TraverserFactory factory;

+

     public readonly ClassTraverser ClassTraverser;

 

     private Bpl.Procedure procedure;

@@ -30,7 +33,7 @@ namespace BytecodeTranslator {
 

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

 

-    internal class MethodParameter {

+    public class MethodParameter {

       public MethodParameter() {

         localParameter = null;

         inParameterCopy = null;

@@ -65,11 +68,11 @@ namespace BytecodeTranslator {
     /// 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>

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

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

-    public Bpl.Variable CreateFreshLocal(ITypeDefinition typedef) {

+    public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {

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

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

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

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

@@ -122,13 +125,16 @@ namespace BytecodeTranslator {
     }

     #endregion

 

-    public MethodTraverser(IContractProvider cp, ClassTraverser cTraverser)

+    public MethodTraverser(TraverserFactory factory, IContractProvider cp, ClassTraverser cTraverser)

       : base(cp) {

+      this.factory = factory;

       HeapVariable = cTraverser.HeapVariable;

       procedure = null;

       ClassTraverser = cTraverser;

     }

 

+    #region Overrides

+

     /// <summary>

     /// 

     /// </summary>

@@ -209,7 +215,7 @@ namespace BytecodeTranslator {
         if (contract != null) {

           try {

             foreach (IPrecondition pre in contract.Preconditions) {

-              ExpressionTraverser exptravers = new ExpressionTraverser(this);

+              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);

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

               // Todo: Deal with Descriptions

 

@@ -221,7 +227,7 @@ namespace BytecodeTranslator {
             }

 

             foreach (IPostcondition post in contract.Postconditions) {

-              ExpressionTraverser exptravers = new ExpressionTraverser(this);

+              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);

 

               exptravers.Visit(post.Condition);

               // Todo: Deal with Descriptions

@@ -233,7 +239,7 @@ namespace BytecodeTranslator {
             }

 

             foreach (IAddressableExpression mod in contract.ModifiedVariables) {

-              ExpressionTraverser exptravers = new ExpressionTraverser(this);

+              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);

               exptravers.Visit(mod);

 

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

@@ -271,7 +277,7 @@ namespace BytecodeTranslator {
           throw new NotImplementedException("abstract methods are not yet implemented");

         }

 

-        StatementTraverser stmtTraverser = new StatementTraverser(this);

+        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this, this.HeapVariable);

 

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

 

@@ -289,7 +295,7 @@ namespace BytecodeTranslator {
         try {

           method.ResolvedMethod.Body.Dispatch(stmtTraverser);

         } catch (TranslationException te) {

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

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

         } catch {

           throw;

         }

@@ -328,5 +334,8 @@ namespace BytecodeTranslator {
       }

     }

 

+    #endregion

+

   }

+

 }

diff --git a/BCT/BytecodeTranslator/Prelude.cs b/BCT/BytecodeTranslator/Prelude.cs
index 6805a39e..6db620ad 100644
--- a/BCT/BytecodeTranslator/Prelude.cs
+++ b/BCT/BytecodeTranslator/Prelude.cs
@@ -4,7 +4,7 @@ using System.IO;
 using System.Text;

 

 namespace BytecodeTranslator {

-  class Prelude {

+  public class Prelude {

     public static void Emit(Microsoft.Boogie.TokenTextWriter wr) {

       wr.Write(@"// Copyright (c) 2010, Microsoft Corp.

 // Bytecode Translator prelude

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index f9e46d0d..452cc114 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -61,7 +61,8 @@ namespace BytecodeTranslator {
 

       #region Pass 3: Translate the code model to BPL

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

-      ToplevelTraverser translator = new ToplevelTraverser(host.GetContractExtractor(module.ModuleIdentity));

+      var factory = new CLRSemantics();

+      ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));

       assembly = module as IAssembly;

       if (assembly != null)

         translator.Visit(assembly);

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index d9c4400a..5ebaea37 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -20,7 +20,10 @@ using System.Diagnostics.Contracts;
 

 namespace BytecodeTranslator

 {

-  internal class StatementTraverser : BaseCodeTraverser {

+  public class StatementTraverser : BaseCodeTraverser {

+

+    public readonly TraverserFactory factory;

+

     public readonly MethodTraverser MethodTraverser;

 

     public readonly Bpl.Variable HeapVariable;

@@ -28,12 +31,11 @@ namespace BytecodeTranslator
     public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();

 

     #region Constructors

-    public StatementTraverser(MethodTraverser mt) {

-      HeapVariable = mt.HeapVariable;

-      MethodTraverser = mt;

-    }

+    public StatementTraverser(TraverserFactory factory, MethodTraverser mt) :

+      this(factory, mt, mt.HeapVariable) { }

 

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

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

+      this.factory = factory;

       HeapVariable = heapvar;

       MethodTraverser = mt;

     }

@@ -46,7 +48,7 @@ namespace BytecodeTranslator
     }

 

     Bpl.Expr ExpressionFor(IExpression expression) {

-      ExpressionTraverser etrav = new ExpressionTraverser(this);

+      ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);

       etrav.Visit(expression);

       Contract.Assert(etrav.TranslatedExpressions.Count == 1);

       return etrav.TranslatedExpressions.Pop();

@@ -82,10 +84,10 @@ namespace BytecodeTranslator
     /// <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);

+      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);

+      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);

 

-      ExpressionTraverser condTraverser = new ExpressionTraverser(this);

+      ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this, this.HeapVariable);

       condTraverser.Visit(conditionalStatement.Condition);

       thenTraverser.Visit(conditionalStatement.TrueBranch);

       elseTraverser.Visit(conditionalStatement.FalseBranch);

@@ -108,7 +110,7 @@ namespace BytecodeTranslator
     /// <remarks> TODO: might be wrong for the general case</remarks>

     public override void Visit(IExpressionStatement expressionStatement) {

 

-      ExpressionTraverser etrav = new ExpressionTraverser(this);

+      ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);

       etrav.Visit(expressionStatement.Expression);

     }

 

@@ -150,7 +152,7 @@ namespace BytecodeTranslator
       #endregion

 

       if (returnStatement.Expression != null) {

-        ExpressionTraverser etrav = new ExpressionTraverser(this);

+        ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);

         etrav.Visit(returnStatement.Expression);

 

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

@@ -202,4 +204,5 @@ namespace BytecodeTranslator
     #endregion

 

   }

+

 }

diff --git a/BCT/BytecodeTranslator/ToplevelTraverser.cs b/BCT/BytecodeTranslator/ToplevelTraverser.cs
index 9079b5af..0ba7bffa 100644
--- a/BCT/BytecodeTranslator/ToplevelTraverser.cs
+++ b/BCT/BytecodeTranslator/ToplevelTraverser.cs
@@ -21,7 +21,9 @@ namespace BytecodeTranslator {
     /// <summary>

     /// 

     /// </summary>

-  internal class ToplevelTraverser : BaseCodeAndContractTraverser {

+  public class ToplevelTraverser : BaseCodeAndContractTraverser {

+

+    public readonly TraverserFactory factory;

 

     public readonly IContractProvider ContractProvider;

 

@@ -29,8 +31,9 @@ namespace BytecodeTranslator {
 

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

 

-    public ToplevelTraverser(IContractProvider cp)

+    public ToplevelTraverser(TraverserFactory factory, IContractProvider cp)

       : base(cp) {

+      this.factory = factory;

       ContractProvider = cp;

       TranslatedProgram = new Bpl.Program();

     }

@@ -38,7 +41,7 @@ namespace BytecodeTranslator {
     public Bpl.Variable FindOrCreateClassField(ITypeDefinition classtype, IFieldDefinition field) {

       ClassTraverser ct;

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

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

+        ct = this.factory.MakeClassTraverser(this, this.contractProvider);

         classMap.Add(classtype, ct);

         return ct.FindOrCreateFieldVariable(field);

       } else {

@@ -55,8 +58,8 @@ namespace BytecodeTranslator {
       if (typeDefinition.IsClass) {

 

         ClassTraverser ct;

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

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

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

+          ct = this.factory.MakeClassTraverser(this, this.contractProvider);

           classMap.Add(typeDefinition, ct);

         }

         ct.Visit(typeDefinition);

@@ -75,4 +78,5 @@ namespace BytecodeTranslator {
     }

 

   }

+

 }

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
new file mode 100644
index 00000000..cacc9817
--- /dev/null
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -0,0 +1,27 @@
+//-----------------------------------------------------------------------------

+//

+// 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 {

+  public abstract class TraverserFactory {

+    public virtual ToplevelTraverser MakeTopLevelTraverser(IContractProvider contractProvider) { return new ToplevelTraverser(this, contractProvider); }

+    public virtual ClassTraverser MakeClassTraverser(ToplevelTraverser parent, IContractProvider contractProvider) { return new ClassTraverser(this, contractProvider, parent); }

+    public virtual MethodTraverser MakeMethodTraverser(ClassTraverser parent, IContractProvider contractProvider) { return new MethodTraverser(this, contractProvider, parent); }

+    public virtual StatementTraverser MakeStatementTraverser(MethodTraverser parent, Bpl.Variable heapVariable) { return new StatementTraverser(this, parent, heapVariable); }

+    public virtual ExpressionTraverser MakeExpressionTraverser(StatementTraverser parent, Bpl.Variable heapVariable) { return new ExpressionTraverser(parent, heapVariable); }

+  }

+}
\ No newline at end of file
diff --git a/BCT/Local.testsettings b/BCT/Local.testsettings
new file mode 100644
index 00000000..f63e9b16
--- /dev/null
+++ b/BCT/Local.testsettings
@@ -0,0 +1,31 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<TestSettings name="Local" id="f898dc7f-7e79-4656-a1cd-5ca50fff2b5d" xmlns="http://microsoft.com/schemas/VisualStudio/TeamTest/2010">

+  <Description>These are default test settings for a local test run.</Description>

+  <Execution>

+    <TestTypeSpecific>

+      <UnitTestRunConfig testTypeId="13cdc9d9-ddb5-4fa4-a97d-d965ccfc6d4b">

+        <AssemblyResolution>

+          <TestDirectory useLoadContext="true" />

+        </AssemblyResolution>

+      </UnitTestRunConfig>

+      <WebTestRunConfiguration testTypeId="4e7599fa-5ecb-43e9-a887-cd63cf72d207">

+        <Browser name="Internet Explorer 7.0">

+          <Headers>

+            <Header name="User-Agent" value="Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 5.1)" />

+            <Header name="Accept" value="*/*" />

+            <Header name="Accept-Language" value="{{$IEAcceptLanguage}}" />

+            <Header name="Accept-Encoding" value="GZIP" />

+          </Headers>

+        </Browser>

+      </WebTestRunConfiguration>

+    </TestTypeSpecific>

+    <AgentRule name="LocalMachineDefaultRole">

+      <DataCollectors>

+        <DataCollector uri="datacollector://microsoft/CodeCoverage/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TestTools.CodeCoverage.CoveragePlugIn, Microsoft.VisualStudio.QualityTools.Plugins.CodeCoverage, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Code Coverage">

+        </DataCollector>

+        <DataCollector uri="datacollector://microsoft/TestImpact/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.TestImpactDataCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Test Impact">

+        </DataCollector>

+      </DataCollectors>

+    </AgentRule>

+  </Execution>

+</TestSettings>
\ No newline at end of file
diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
new file mode 100644
index 00000000..f537f861
--- /dev/null
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -0,0 +1,15 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics.Contracts;

+

+namespace RegressionTestInput {

+  public class Class0 {

+    void M(int x) {

+      int y = (5 / x) + (x = 3);

+      Contract.Assert(x == 3 && y <= 8);

+    }

+

+  }

+}

diff --git a/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs b/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..b3cc080a
--- /dev/null
+++ b/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("RegressionTestInput")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("RegressionTestInput")]

+[assembly: AssemblyCopyright("Copyright ©  2010")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("dc8e9afb-ef4e-4954-8f86-1a79bb0d77e4")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj b/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj
new file mode 100644
index 00000000..6cf94c40
--- /dev/null
+++ b/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj
@@ -0,0 +1,54 @@
+<?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>8.0.30703</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>RegressionTestInput</RootNamespace>

+    <AssemblyName>RegressionTestInput</AssemblyName>

+    <TargetFrameworkVersion>v4.0</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>

+  </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="System" />

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

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

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

+    <Reference Include="Microsoft.CSharp" />

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

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

+  </ItemGroup>

+  <ItemGroup>

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

+    <Compile Include="Properties\AssemblyInfo.cs" />

+  </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/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs b/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..a0fd3275
--- /dev/null
+++ b/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs
@@ -0,0 +1,35 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("TranslationTest")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("TranslationTest")]

+[assembly: AssemblyCopyright("Copyright ©  2010")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("f448ac99-c5e7-424c-8bdb-243e8276d4d7")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
new file mode 100644
index 00000000..564dd07e
--- /dev/null
+++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
@@ -0,0 +1,50 @@
+// Copyright (c) 2010, Microsoft Corp.

+// Bytecode Translator prelude

+

+type Ref;

+const null: Ref;

+

+type Field alpha;

+

+type HeapType = <alpha>[Ref, Field alpha]alpha;

+function IsGoodHeap(HeapType): bool;

+

+var $Heap: HeapType where IsGoodHeap($Heap);

+

+procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int);

+

+

+

+implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)

+{

+  var __temp_1: int;

+  var $tmp0: int;

+  var __temp_2: int;

+  var __temp_3: int;

+  var local_0: int;

+  var x: int;

+

+    x := x$in;

+    $tmp0 := x;

+    assert $tmp0 != 0;

+    __temp_1 := 5 / $tmp0;

+    __temp_2 := 3;

+    __temp_3 := __temp_2;

+    x := __temp_3;

+    local_0 := __temp_1 + __temp_2;

+    assert x == 3 && local_0 <= 8;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.Class0..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
new file mode 100644
index 00000000..f0520a8f
--- /dev/null
+++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
@@ -0,0 +1,111 @@
+<?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>

+    </ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{A112AFBA-D6F6-44A4-A683-C3D458A68D84}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>TranslationTest</RootNamespace>

+    <AssemblyName>TranslationTest</AssemblyName>

+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <ProjectTypeGuids>{3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>

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

+  </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="Core">

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

+    </Reference>

+    <Reference Include="Microsoft.VisualStudio.QualityTools.UnitTestFramework, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

+    <Reference Include="System" />

+    <Reference Include="System.Core">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

+  </ItemGroup>

+  <ItemGroup>

+    <CodeAnalysisDependentAssemblyPaths Condition=" '$(VS100COMNTOOLS)' != '' " Include="$(VS100COMNTOOLS)..\IDE\PrivateAssemblies">

+      <Visible>False</Visible>

+    </CodeAnalysisDependentAssemblyPaths>

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="Properties\AssemblyInfo.cs" />

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

+  </ItemGroup>

+  <ItemGroup>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\MetadataHelper.csproj">

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

+      <Name>MetadataHelper</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MetadataModel\MetadataModel.csproj">

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

+      <Name>MetadataModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MutableMetadataModel\MutableMetadataModel.csproj">

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

+      <Name>MutableMetadataModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\PdbReader\PdbReader.csproj">

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

+      <Name>PdbReader</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\PeReader\PeReader.csproj">

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

+      <Name>PeReader</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\SourceModel\SourceModel.csproj">

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

+      <Name>SourceModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\CodeModel\CodeModel.csproj">

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

+      <Name>CodeModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\ILToCodeModel\ILToCodeModel.csproj">

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

+      <Name>ILToCodeModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\MutableCodeModel\MutableCodeModel.csproj">

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

+      <Name>MutableCodeModel</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\..\BytecodeTranslator\BytecodeTranslator.csproj">

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

+      <Name>BytecodeTranslator</Name>

+    </ProjectReference>

+    <ProjectReference Include="..\RegressionTestInput\RegressionTestInput.csproj">

+      <Project>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</Project>

+      <Name>RegressionTestInput</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

+    <EmbeddedResource Include="RegressionTestInput.txt" />

+  </ItemGroup>

+  <Import Project="$(MSBuildBinPath)\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/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
new file mode 100644
index 00000000..a018797d
--- /dev/null
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -0,0 +1,119 @@
+using System;

+using System.Text;

+using System.Collections.Generic;

+using System.Linq;

+using Microsoft.VisualStudio.TestTools.UnitTesting;

+using System.IO;

+using Microsoft.Cci;

+using Microsoft.Cci.MetadataReader;

+using Microsoft.Cci.MutableCodeModel;

+using Microsoft.Cci.Contracts;

+using Microsoft.Cci.ILToCodeModel;

+using BytecodeTranslator;

+

+namespace TranslationTest {

+  /// <summary>

+  /// Summary description for UnitTest0

+  /// </summary>

+  [TestClass]

+  public class UnitTest0 {

+    public UnitTest0() {

+      //

+      // TODO: Add constructor logic here

+      //

+    }

+

+    private TestContext testContextInstance;

+

+    /// <summary>

+    ///Gets or sets the test context which provides

+    ///information about and functionality for the current test run.

+    ///</summary>

+    public TestContext TestContext {

+      get {

+        return testContextInstance;

+      }

+      set {

+        testContextInstance = value;

+      }

+    }

+

+    #region Additional test attributes

+    //

+    // You can use the following additional attributes as you write your tests:

+    //

+    // Use ClassInitialize to run code before running the first test in the class

+    // [ClassInitialize()]

+    // public static void MyClassInitialize(TestContext testContext) { }

+    //

+    // Use ClassCleanup to run code after all tests in a class have run

+    // [ClassCleanup()]

+    // public static void MyClassCleanup() { }

+    //

+    // Use TestInitialize to run code before running each test 

+    // [TestInitialize()]

+    // public void MyTestInitialize() { }

+    //

+    // Use TestCleanup to run code after each test has run

+    // [TestCleanup()]

+    // public void MyTestCleanup() { }

+    //

+    #endregion

+

+    private string ExecuteTest(string assemblyName) {

+

+      var host = new Microsoft.Cci.ILToCodeModel.CodeContractAwareHostEnvironment();

+      BCT.Host = host;

+

+      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.");

+        Assert.Fail("Failed to read in test assembly for regression test");

+      }

+

+      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);

+      }

+

+      module = Decompiler.GetCodeAndContractModelFromMetadataModel(host, module, pdbReader);

+

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

+      var factory = new CLRSemantics();

+      ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));

+      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(module.Name + ".bpl");

+      Prelude.Emit(writer);

+      translator.TranslatedProgram.Emit(writer);

+      writer.Close();

+      var fileName = Path.ChangeExtension(assemblyName, "bpl");

+      var s = File.ReadAllText(fileName);

+      return s;

+    }

+

+    [TestMethod]

+    public void TranslationTest() {

+      string dir = TestContext.DeploymentDirectory;

+      var fullPath = Path.Combine(dir, "RegressionTestInput.dll");

+      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.RegressionTestInput.txt");

+      StreamReader reader = new StreamReader(resource);

+      string expected = reader.ReadToEnd();

+      var result = ExecuteTest(fullPath);

+      if (result != expected) {

+        string resultFile = Path.GetFullPath("RegressionTestOutput.txt");

+        File.WriteAllText(resultFile, result);

+        Assert.Fail("Output didn't match RegressionTestInput.txt: " + resultFile);

+      }

+    }

+  }

+}

+ 
\ No newline at end of file
diff --git a/BCT/TraceAndTestImpact.testsettings b/BCT/TraceAndTestImpact.testsettings
new file mode 100644
index 00000000..a6b85f3a
--- /dev/null
+++ b/BCT/TraceAndTestImpact.testsettings
@@ -0,0 +1,21 @@
+<?xml version="1.0" encoding="UTF-8"?>

+<TestSettings name="Trace and Test Impact" id="cadf610f-d4f6-4ea8-9e0b-470bc35c9956" xmlns="http://microsoft.com/schemas/VisualStudio/TeamTest/2010">

+  <Description>These are test settings for Trace and Test Impact.</Description>

+  <Execution>

+    <TestTypeSpecific />

+    <AgentRule name="Execution Agents">

+      <DataCollectors>

+        <DataCollector uri="datacollector://microsoft/SystemInfo/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TestTools.DataCollection.SystemInfo.SystemInfoDataCollector, Microsoft.VisualStudio.TestTools.DataCollection.SystemInfo, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="System Information">

+        </DataCollector>

+        <DataCollector uri="datacollector://microsoft/ActionLog/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TestTools.ManualTest.ActionLog.ActionLogPlugin, Microsoft.VisualStudio.TestTools.ManualTest.ActionLog, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Actions">

+        </DataCollector>

+        <DataCollector uri="datacollector://microsoft/HttpProxy/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.HttpProxyCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="ASP.NET Client Proxy for IntelliTrace and Test Impact">

+        </DataCollector>

+        <DataCollector uri="datacollector://microsoft/TestImpact/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.TestImpactDataCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="Test Impact">

+        </DataCollector>

+        <DataCollector uri="datacollector://microsoft/TraceDebugger/1.0" assemblyQualifiedName="Microsoft.VisualStudio.TraceCollector.TraceDebuggerDataCollector, Microsoft.VisualStudio.TraceCollector, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" friendlyName="IntelliTrace">

+        </DataCollector>

+      </DataCollectors>

+    </AgentRule>

+  </Execution>

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