Introduction of the Sink: a global object that is threaded through all of the traversers and which contains the information that they need to share with each other.

8 files changed, 91 insertions, 146 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 0a7d6d55..5867c90c 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -112,6 +112,7 @@
     <Compile Include="MetadataTraverser.cs" />

     <Compile Include="Prelude.cs" />

     <Compile Include="ExpressionTraverser.cs" />

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

     <Compile Include="StatementTraverser.cs" />

     <Compile Include="Program.cs" />

     <Compile Include="TranslationException.cs" />

diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
index c9f09f5f..78077ef3 100644
--- a/BCT/BytecodeTranslator/CLRSemantics.cs
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -20,14 +20,14 @@ namespace BytecodeTranslator {
 

   public class CLRSemantics : TraverserFactory {

 

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

-      return new CLRExpressionSemantics(parent, heapVariable);

+    public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) {

+      return new CLRExpressionSemantics(sink, statementTraverser);

     }

 

     public class CLRExpressionSemantics : ExpressionTraverser {

 

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

-        : base(stmtTraverser, heapvar) { }

+      public CLRExpressionSemantics(Sink sink, StatementTraverser/*?*/ statementTraverser)

+        : base(sink, statementTraverser) { }

 

       public override void Visit(IDivision division) {

         this.Visit(division.LeftOperand);

@@ -37,7 +37,7 @@ namespace BytecodeTranslator {
 

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

 

-        var loc = this.StmtTraverser.MetadataTraverser.CreateFreshLocal(division.RightOperand.Type);

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

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

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

         this.StmtTraverser.StmtBuilder.Add(storeLocal);

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index a8f9a758..041998fa 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -24,19 +24,30 @@ namespace BytecodeTranslator {
     // 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;

 

+    protected readonly Sink sink;

+

+    protected readonly StatementTraverser StmtTraverser;

+

     #region Constructors

 

-    public ExpressionTraverser(StatementTraverser stmtTraverser) 

-      : this(stmtTraverser, stmtTraverser.HeapVariable)

+    /// <summary>

+    /// Use this constructor for translating expressions that do *not* occur

+    /// within the context of the statements in a method body.

+    /// </summary>

+    public ExpressionTraverser(Sink sink)

+      : this(sink, null)

     { }

 

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

-      HeapVariable = heapvar;

-      StmtTraverser = stmtTraverser;

+    /// <summary>

+    /// Use this constructor for translating expressions that do occur within

+    /// the context of the statements in a method body.

+    /// </summary>

+    public ExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) {

+      this.sink = sink;

+      HeapVariable = sink.HeapVariable;

+      this.StmtTraverser = statementTraverser;

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

     }

 

@@ -52,12 +63,12 @@ namespace BytecodeTranslator {
     public override void Visit(IAddressableExpression addressableExpression) {

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

       if (local != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));

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

         return;

       }

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

       if (param != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));

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

         return;

       }

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

@@ -125,7 +136,7 @@ namespace BytecodeTranslator {
       #region LocalDefinition

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

       if (local != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));

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

         return;

       }

       #endregion

@@ -133,7 +144,7 @@ namespace BytecodeTranslator {
       #region ParameterDefenition

       IParameterDefinition param = targetExpression.Definition as IParameterDefinition;

       if (param != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));

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

         return;

       }

       #endregion

@@ -156,7 +167,7 @@ namespace BytecodeTranslator {
     

     public override void Visit(IThisReference thisReference) {

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

-        this.StmtTraverser.MetadataTraverser.ThisVariable));

+        this.sink.ThisVariable));

     }

 

     public override void Visit(IBoundExpression boundExpression) {

@@ -168,7 +179,7 @@ namespace BytecodeTranslator {
       #region LocalDefinition

       ILocalDefinition local = boundExpression.Definition as ILocalDefinition;

       if (local != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));

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

         return;

       }

       #endregion

@@ -176,7 +187,7 @@ namespace BytecodeTranslator {
       #region ParameterDefiniton

       IParameterDefinition param = boundExpression.Definition as IParameterDefinition;

       if (param != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));

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

         return;

       }

       #endregion

@@ -248,7 +259,7 @@ namespace BytecodeTranslator {
 

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

       TranslatedExpressions.Push( Bpl.Expr.Ident( 

-        this.StmtTraverser.MetadataTraverser.FindOrCreateFieldVariable(field.ResolvedField) ) );

+        this.sink.FindOrCreateFieldVariable(field.ResolvedField) ) );

 

       this.Visit(instance);

 

@@ -345,7 +356,7 @@ namespace BytecodeTranslator {
         #endregion

 

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

-          Bpl.Variable v = this.StmtTraverser.MetadataTraverser.CreateFreshLocal(methodCall.Type.ResolvedType);

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

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

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

         }

@@ -529,11 +540,11 @@ namespace BytecodeTranslator {
     }

     

     public override void Visit(IReturnValue returnValue) {

-      if (this.StmtTraverser.MetadataTraverser.RetVariable == null) {

+      if (this.sink.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.MetadataTraverser.RetVariable));

+        this.sink.RetVariable));

 

     }

     #endregion

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 661e240f..bba3515a 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -25,85 +25,31 @@ namespace BytecodeTranslator {
   /// </summary>

   public class MetadataTraverser : BaseMetadataTraverser {

 

+    readonly Sink sink;

+

     public readonly TraverserFactory factory;

 

     public readonly IContractProvider ContractProvider;

 

-    public readonly Bpl.Program TranslatedProgram;

-

     public Bpl.Variable HeapVariable;

     

-    private Dictionary<IFieldDefinition, Bpl.GlobalVariable> fieldVarMap = null;

 

-    public MetadataTraverser(TraverserFactory factory, IContractProvider cp)

+    public MetadataTraverser(Sink sink, IContractProvider cp)

       : base() {

-      this.factory = factory;

+      this.sink = sink;

+      this.factory = sink.Factory;

       ContractProvider = cp;

-      TranslatedProgram = new Bpl.Program();

-    }

-

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

-        this.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Constant(tok, tident, true));

-      }

-      return v;

     }

 

-    public class MethodParameter {

-      public MethodParameter() {

-        localParameter = null;

-        inParameterCopy = null;

-        outParameterCopy = null;

-      }

 

-      public Bpl.Formal localParameter;

-      public Bpl.Formal inParameterCopy;

-      public Bpl.Formal outParameterCopy;

+    public Bpl.Program TranslatedProgram {

+      get { return this.sink.TranslatedProgram; }

     }

 

     #region Method Helpers

     /// <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="typeReference"> The type of the new variable </param>

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

-    public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {

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

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

-      return v;

-    }

-

-    /// <summary>

-    /// 

-    /// </summary>

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

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

     private MethodParameter CreateBoogieParameter(IParameterDefinition param) {

@@ -134,17 +80,6 @@ namespace BytecodeTranslator {
       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 Method Helpers

 

     #region Overrides

@@ -162,20 +97,12 @@ namespace BytecodeTranslator {
     /// </summary>

     /// 

 

-    #region Local state for each type

-    // TODO: (mschaef) just a stub

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

-    #endregion

 

     public override void Visit(ITypeDefinition typeDefinition) {

 

-      var savedFieldVarMap = this.fieldVarMap;

-      this.fieldVarMap = new Dictionary<IFieldDefinition, Microsoft.Boogie.GlobalVariable>(); 

-

       if (typeDefinition.IsClass) {

 

         base.Visit(typeDefinition);

-        this.fieldVarMap = savedFieldVarMap;

 

       } else {

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

@@ -185,11 +112,6 @@ namespace BytecodeTranslator {
 

     #region Local state for each method

 

-    private Dictionary<IParameterDefinition, MethodParameter> formalMap = null;

-    internal Bpl.Variable RetVariable;

-    internal List<MethodParameter> OutVars = new List<MethodParameter>();

-    private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = null;

-

     #endregion

 

     /// <summary>

@@ -197,8 +119,8 @@ namespace BytecodeTranslator {
     /// </summary>

     public override void Visit(IMethodDefinition method) {

 

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

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

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

+      this.sink.BeginMethod();

 

       try {

         #region Create in- and out-parameters

@@ -213,6 +135,7 @@ namespace BytecodeTranslator {
           if (mp.outParameterCopy != null) out_count++;

           formalMap.Add(formal, mp);

         }

+        this.sink.FormalMap = formalMap;

 

         #region Look for Returnvalue

 

@@ -220,11 +143,11 @@ namespace BytecodeTranslator {
         if (method.Type.TypeCode != PrimitiveTypeCode.Void) {

           Bpl.Type rettype = Bpl.Type.Int;

           out_count++;

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

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

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

                   "$result", rettype), false);

         } else {

-          RetVariable = null;

+          this.sink.RetVariable = null;

         }

 

         #endregion

@@ -254,12 +177,12 @@ namespace BytecodeTranslator {
           }

           if (mparam.outParameterCopy != null) {

             outvars[j++] = mparam.outParameterCopy;

-            OutVars.Add(mparam);

+            this.sink.OutVars.Add(mparam);

           }

         }

 

         #region add the returnvalue to out if there is one

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

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

         #endregion

 

         #endregion

@@ -274,7 +197,7 @@ namespace BytecodeTranslator {
         if (contract != null) {

           try {

             foreach (IPrecondition pre in contract.Preconditions) {

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

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

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

               // Todo: Deal with Descriptions

 

@@ -286,7 +209,7 @@ namespace BytecodeTranslator {
             }

 

             foreach (IPostcondition post in contract.Postconditions) {

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

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

 

               exptravers.Visit(post.Condition);

               // Todo: Deal with Descriptions

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

 

             foreach (IAddressableExpression mod in contract.ModifiedVariables) {

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

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

               exptravers.Visit(mod);

 

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

@@ -328,13 +251,13 @@ namespace BytecodeTranslator {
             boogieModifies,

             boogiePostcondition);

 

-        this.TranslatedProgram.TopLevelDeclarations.Add(proc);

+        this.sink.TranslatedProgram.TopLevelDeclarations.Add(proc);

 

         if (method.IsAbstract) {

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

         }

 

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

+        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink);

 

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

 

@@ -359,9 +282,9 @@ namespace BytecodeTranslator {
 

         #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];

+        Bpl.Variable[] vars = new Bpl.Variable[this.sink.LocalVarMap.Values.Count + formalMap.Values.Count];

         i = 0;

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

+        foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

           vars[i++] = v;

         }

         foreach (MethodParameter mparam in formalMap.Values) {

@@ -381,7 +304,7 @@ namespace BytecodeTranslator {
                 stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));

 

         impl.Proc = proc;

-        this.TranslatedProgram.TopLevelDeclarations.Add(impl);

+        this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

       } catch (TranslationException te) {

         throw new NotImplementedException(te.ToString());

       } catch {

@@ -392,7 +315,7 @@ namespace BytecodeTranslator {
     }

 

     public override void Visit(IFieldDefinition fieldDefinition) {

-      this.FindOrCreateFieldVariable(fieldDefinition);

+      this.sink.FindOrCreateFieldVariable(fieldDefinition);

     }

 

     #endregion

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 14cbfce7..139188bb 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -62,7 +62,7 @@ namespace BytecodeTranslator {
       #region Pass 3: Translate the code model to BPL

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

       var factory = new CLRSemantics();

-      MetadataTraverser translator = new MetadataTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));

+      MetadataTraverser translator = factory.MakeMetadataTraverser(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 af053d2d..c528e846 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -24,20 +24,17 @@ namespace BytecodeTranslator
 

     public readonly TraverserFactory factory;

 

-    public readonly MetadataTraverser MetadataTraverser;

+    readonly Sink sink;

 

-    public readonly Bpl.Variable HeapVariable;

+    private readonly Bpl.Variable HeapVariable;

 

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

 

     #region Constructors

-    public StatementTraverser(TraverserFactory factory, MetadataTraverser mt) :

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

-

-    public StatementTraverser(TraverserFactory factory, MetadataTraverser mt, Bpl.Variable heapvar) {

-      this.factory = factory;

-      HeapVariable = heapvar;

-      MetadataTraverser = mt;

+    public StatementTraverser(Sink sink) {

+      this.sink = sink;

+      this.factory = sink.Factory;

+      HeapVariable = sink.HeapVariable;

     }

     #endregion

 

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

 

     Bpl.Expr ExpressionFor(IExpression expression) {

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

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

       etrav.Visit(expression);

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

       return etrav.TranslatedExpressions.Pop();

@@ -84,10 +81,10 @@ namespace BytecodeTranslator
     /// <remarks>(mschaef) Works, but still a stub</remarks>

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

     public override void Visit(IConditionalStatement conditionalStatement) {

-      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.MetadataTraverser, this.HeapVariable);

-      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.MetadataTraverser, this.HeapVariable);

+      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink);

+      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink);

 

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

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

       condTraverser.Visit(conditionalStatement.Condition);

       thenTraverser.Visit(conditionalStatement.TrueBranch);

       elseTraverser.Visit(conditionalStatement.FalseBranch);

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

     public override void Visit(IExpressionStatement expressionStatement) {

 

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

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

       etrav.Visit(expressionStatement.Expression);

     }

 

@@ -129,7 +126,7 @@ namespace BytecodeTranslator
     /// </summary>

     public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {

       if (localDeclarationStatement.InitialValue == null) return;

-      var loc = this.MetadataTraverser.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

+      var loc = this.sink.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

       var tok = TokenFor(localDeclarationStatement);

       var e = ExpressionFor(localDeclarationStatement.InitialValue);

       StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));

@@ -145,22 +142,22 @@ namespace BytecodeTranslator
       Bpl.IToken tok = TokenFor(returnStatement);

 

       #region Copy values of all out parameters to outvariables

-      foreach (MetadataTraverser.MethodParameter mp in this.MetadataTraverser.OutVars) {

+      foreach (MethodParameter mp in this.sink.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 = this.factory.MakeExpressionTraverser(this, this.HeapVariable);

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

         etrav.Visit(returnStatement.Expression);

 

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

+        if (this.sink.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.MetadataTraverser.RetVariable), etrav.TranslatedExpressions.Pop()));

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

       }

       StmtBuilder.Add(new Bpl.ReturnCmd(TokenFor(returnStatement)));

     }

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 9086290a..dfebaa53 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -18,6 +18,19 @@ using Bpl = Microsoft.Boogie;
 

 

 namespace BytecodeTranslator {

+

+  public class MethodParameter {

+    public MethodParameter() {

+      localParameter = null;

+      inParameterCopy = null;

+      outParameterCopy = null;

+    }

+

+    public Bpl.Formal localParameter;

+    public Bpl.Formal inParameterCopy;

+    public Bpl.Formal outParameterCopy;

+  }

+

     /// <summary>

     /// Class containing several static helper functions to convert

     /// from Cci to Boogie Methodology

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 9f79b034..4a48cf5f 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -18,8 +18,8 @@ using Bpl = Microsoft.Boogie;
 

 namespace BytecodeTranslator {

   public abstract class TraverserFactory {

-    public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider) { return new MetadataTraverser(this, contractProvider); }

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

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

+    public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider) { return new MetadataTraverser(new Sink(this), contractProvider); }

+    public virtual StatementTraverser MakeStatementTraverser(Sink sink) { return new StatementTraverser(sink); }

+    public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser) { return new ExpressionTraverser(sink, statementTraverser); }

   }

 }
\ No newline at end of file