1 files changed, 79 insertions, 0 deletions
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);
+    }
+
+  }
+}