Major changes to the translator traversers because they now are based on the

new traversers. (The old ones have been marked as obsolete.)
All types are now encoded as "datatypes" in Boogie. So non-generic types are
nullary functions and generic types just have at least one type argument.
Lots of other fixes: string encoding of names is now done by negating Boogie's
regular expression for identifiers, etc.

18 files changed, 489 insertions, 489 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index cc51aaf9..dbcc8dad 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -1452,7 +1452,7 @@ namespace BytecodeTranslator
       //  new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),

       //  new Bpl.ExprSeq(new Bpl.IdentifierExpr(checkIfInstance.Token(), v))

       //  );

-      base.TraverseChildren(checkIfInstance.Operand);

+      base.Traverse(checkIfInstance.Operand);

       var exp = TranslatedExpressions.Pop();

       var dynTypeOfOperand = this.sink.Heap.DynamicType(exp);

       //var subtype = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Subtype, dynTypeOfOperand, e);

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 727d09c5..45adb36e 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -114,7 +114,7 @@ namespace BytecodeTranslator {
     [RepresentationFor("null", "const unique null : Ref;")]

     public Bpl.Constant NullRef;

 

-    [RepresentationFor("Type", "type Type;")]

+    [RepresentationFor("Type", "type {:datatype} Type;")]

     public Bpl.TypeCtorDecl TypeTypeDecl = null;

     public Bpl.CtorType TypeType;

 

@@ -258,12 +258,8 @@ namespace BytecodeTranslator {
     /// </summary>

     public Bpl.Variable CreateTypeVariable(ITypeReference type, List<Bpl.ConstantParent> parents)

     {

-        string typename = TypeHelper.GetTypeName(type);

+      string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);

         typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);

-        // Need to append something to the name to avoid name clashes with other members (of a different

-        // type) that have the same name.

-        typename += "$type";

-

         Bpl.IToken tok = type.Token();

         Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, this.TypeType);

         Bpl.Constant v = new Bpl.Constant(tok, tident, true /*unique*/, parents, false, null);

@@ -271,18 +267,21 @@ namespace BytecodeTranslator {
     }

 

     public Bpl.Function CreateTypeFunction(ITypeReference type, int parameterCount) {

-      System.Diagnostics.Debug.Assert(parameterCount > 0);

-      string typename = TypeHelper.GetTypeName(type);

+      System.Diagnostics.Debug.Assert(parameterCount >= 0);

+      string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);

       typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);

-      // Need to append something to the name to avoid name clashes.

-      typename += "$type";

       Bpl.IToken tok = type.Token();

       Bpl.VariableSeq inputs = new Bpl.VariableSeq();

-      for (int i = 0; i < parameterCount; i++) {

-        inputs.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "arg"+i, this.TypeType), true));

+      //for (int i = 0; i < parameterCount; i++) {

+      //  inputs.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "arg"+i, this.TypeType), true));

+      //}

+      foreach (var t in type.ResolvedType.GenericParameters) {

+        inputs.Add(new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, t.Name.Value, this.TypeType), true));

       }

       Bpl.Variable output = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "result", this.TypeType), false);

       Bpl.Function func = new Bpl.Function(tok, typename, inputs, output);

+      var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "constructor", new List<object>(1), null);

+      func.Attributes = attrib;

       return func;

     }

     

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 19339962..4f0e3667 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -27,7 +27,7 @@ namespace BytecodeTranslator {
   /// Responsible for traversing all metadata elements (i.e., everything exclusive

   /// of method bodies).

   /// </summary>

-  public class MetadataTraverser : BaseMetadataTraverser {

+  public class BCTMetadataTraverser : MetadataTraverser {

 

     readonly Sink sink;

     public readonly TraverserFactory Factory;

@@ -35,7 +35,7 @@ namespace BytecodeTranslator {
     public readonly IDictionary<IUnit, PdbReader> PdbReaders;

     public PdbReader/*?*/ PdbReader;

 

-    public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders, TraverserFactory factory)

+    public BCTMetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders, TraverserFactory factory)

       : base() {

       this.sink = sink;

       this.Factory = factory;

@@ -47,7 +47,7 @@ namespace BytecodeTranslator {
       foreach (IPrecondition pre in contract.Preconditions) {

         var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);

         ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);

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

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

         // Todo: Deal with Descriptions

         var req = new Bpl.Requires(pre.Token(), false, exptravers.TranslatedExpressions.Pop(), "");

         translatedPres.Add(req);

@@ -61,7 +61,7 @@ namespace BytecodeTranslator {
       foreach (IPostcondition post in contract.Postconditions) {

         var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);

         ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);

-        exptravers.Visit(post.Condition);

+        exptravers.Traverse(post.Condition);

         // Todo: Deal with Descriptions

         var ens = new Bpl.Ensures(post.Token(), false, exptravers.TranslatedExpressions.Pop(), "");

         translatedPosts.Add(ens);

@@ -74,7 +74,7 @@ namespace BytecodeTranslator {
       ICollection<Bpl.IdentifierExpr> modifiedExpr = new List<Bpl.IdentifierExpr>();

       foreach (IAddressableExpression mod in contract.ModifiedVariables) {

         ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, null, true);

-        exptravers.Visit(mod);

+        exptravers.Traverse(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()));

@@ -88,16 +88,16 @@ namespace BytecodeTranslator {
 

     #region Overrides

 

-    public override void Visit(IModule module) {

+    public override void TraverseChildren(IModule module) {

       this.PdbReaders.TryGetValue(module, out this.PdbReader);

-      base.Visit(module);

+      base.TraverseChildren(module);

     }

 

-    public override void Visit(IAssembly assembly) {

+    public override void TraverseChildren(IAssembly assembly) {

       this.PdbReaders.TryGetValue(assembly, out this.PdbReader);

       this.sink.BeginAssembly(assembly);

       try {

-        base.Visit(assembly);

+        base.TraverseChildren(assembly);

       } finally {

         this.sink.EndAssembly(assembly);

       }

@@ -107,7 +107,7 @@ namespace BytecodeTranslator {
     /// Translate the type definition.

     /// </summary>

     /// 

-    public override void Visit(ITypeDefinition typeDefinition) {

+    public override void TraverseChildren(ITypeDefinition typeDefinition) {

 

       if (!this.sink.TranslateType(typeDefinition)) return;

 

@@ -117,11 +117,16 @@ namespace BytecodeTranslator {
       trackPhonePageNameVariableName(typeDefinition);

       trackPhoneApplicationClassname(typeDefinition);

 

+      var gtp = typeDefinition as IGenericTypeParameter;

+      if (gtp != null) {

+        return;

+      }

+

       if (typeDefinition.IsClass) {

         bool savedSawCctor = this.sawCctor;

         this.sawCctor = false;

-        sink.FindOrCreateType(typeDefinition);

-        base.Visit(typeDefinition);

+        sink.FindOrCreateTypeReference(typeDefinition);

+        base.TraverseChildren(typeDefinition);

         if (!this.sawCctor) {

           CreateStaticConstructor(typeDefinition);

         }

@@ -130,23 +135,23 @@ namespace BytecodeTranslator {
         ITypeDefinition unspecializedType = Microsoft.Cci.MutableContracts.ContractHelper.Unspecialized(typeDefinition).ResolvedType;

         sink.AddDelegateType(unspecializedType);

       } else if (typeDefinition.IsInterface) {

-        sink.FindOrCreateType(typeDefinition);

-        base.Visit(typeDefinition);

+        sink.FindOrCreateTypeReference(typeDefinition);

+        base.TraverseChildren(typeDefinition);

       } else if (typeDefinition.IsEnum) {

         return; // enums just are translated as ints

       } else if (typeDefinition.IsStruct) {

-        sink.FindOrCreateType(typeDefinition);

+        sink.FindOrCreateTypeReference(typeDefinition);

         CreateDefaultStructConstructor(typeDefinition);

         CreateStructCopyConstructor(typeDefinition);

-        base.Visit(typeDefinition);

+        base.TraverseChildren(typeDefinition);

       } else {

         Console.WriteLine("Unknown kind of type definition '{0}' was found",

           TypeHelper.GetTypeName(typeDefinition));

         throw new NotImplementedException(String.Format("Unknown kind of type definition '{0}'.", TypeHelper.GetTypeName(typeDefinition)));

       }

-      this.Visit(typeDefinition.PrivateHelperMembers);

+      this.Traverse(typeDefinition.PrivateHelperMembers);

       foreach (var t in this.privateTypes) {

-        this.Visit(t);

+        this.Traverse(t);

       }

     }

     List<ITypeDefinition> privateTypes = new List<ITypeDefinition>();

@@ -221,7 +226,7 @@ namespace BytecodeTranslator {
         };

       }

 

-      stmtTranslator.Visit(stmts);

+      stmtTranslator.Traverse(stmts);

       var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);

 

       var lit = Bpl.Expr.Literal(1);

@@ -325,7 +330,7 @@ namespace BytecodeTranslator {
           });

       }

 

-      stmtTranslator.Visit(stmts);

+      stmtTranslator.Traverse(stmts);

       var translatedStatements = stmtTranslator.StmtBuilder.Collect(Bpl.Token.NoToken);

 

       List<Bpl.Variable> vars = new List<Bpl.Variable>();

@@ -352,7 +357,7 @@ namespace BytecodeTranslator {
     /// <summary>

     /// 

     /// </summary>

-    public override void Visit(IMethodDefinition method) {

+    public override void TraverseChildren(IMethodDefinition method) {

 

       if (method.IsStaticConstructor) this.sawCctor = true;

 

@@ -406,7 +411,7 @@ namespace BytecodeTranslator {
 

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

 

-        foreach (MethodParameter mparam in formalMap.Values) {

+        foreach (MethodParameter mparam in formalMap) {

           if (mparam.inParameterCopy != null) {

             Bpl.IToken tok = method.Token();

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

@@ -420,7 +425,9 @@ namespace BytecodeTranslator {
         #region For non-deferring ctors and all cctors, initialize all fields to null-equivalent values

         var inits = InitializeFieldsInConstructor(method);

         if (0 < inits.Count) {

-          new BlockStatement() { Statements = inits, }.Dispatch(stmtTraverser);

+          foreach (var s in inits) {

+            stmtTraverser.Traverse(s);

+          }

         }

         #endregion

 

@@ -481,7 +488,7 @@ namespace BytecodeTranslator {
 

         #region Create Local Vars For Implementation

         List<Bpl.Variable> vars = new List<Bpl.Variable>();

-        foreach (MethodParameter mparam in formalMap.Values) {

+        foreach (MethodParameter mparam in formalMap) {

           if (!mparam.underlyingParameter.IsByReference)

             vars.Add(mparam.outParameterCopy);

         }

@@ -597,7 +604,7 @@ namespace BytecodeTranslator {
       return referencedTypeDefinition;

     }

 

-    public override void Visit(IFieldDefinition fieldDefinition) {

+    public override void TraverseChildren(IFieldDefinition fieldDefinition) {

       Bpl.Variable fieldVar= this.sink.FindOrCreateFieldVariable(fieldDefinition);

 

       // if tracked by the phone plugin, we need to find out the bpl assigned name for future use

@@ -642,31 +649,30 @@ namespace BytecodeTranslator {
         addPhoneTopLevelDeclarations();

 

       foreach (var a in assemblies) {

-        a.Dispatch(this);

+        this.Traverse((IAssembly)a);

       }

     }

     #endregion

 

     #region Helpers

-    private class FindCtorCall : BaseCodeTraverser {

+    private class FindCtorCall : CodeTraverser {

       private bool isDeferringCtor = false;

       public ITypeReference containingType;

       public static bool IsDeferringCtor(IMethodDefinition method, IBlockStatement body) {

         var fcc = new FindCtorCall(method.ContainingType);

-        fcc.Visit(body);

+        fcc.Traverse(body);

         return fcc.isDeferringCtor;

       }

       private FindCtorCall(ITypeReference containingType) {

         this.containingType = containingType;

       }

-      public override void Visit(IMethodCall methodCall) {

+      public override void TraverseChildren(IMethodCall methodCall) {

         var md = methodCall.MethodToCall.ResolvedMethod;

         if (md != null && md.IsConstructor && methodCall.ThisArgument is IThisReference) {

           this.isDeferringCtor = TypeHelper.TypesAreEquivalent(md.ContainingType, containingType);

-          this.stopTraversal = true;

           return;

         }

-        base.Visit(methodCall);

+        base.TraverseChildren(methodCall);

       }

     }

 

diff --git a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
index 066d4cdf..a5ed9cf3 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
@@ -6,7 +6,7 @@ using Microsoft.Cci;
 using Microsoft.Cci.MutableCodeModel;

 

 namespace BytecodeTranslator.Phone {

-  class PhoneBackKeyCallbackTraverser : BaseCodeTraverser {

+  class PhoneBackKeyCallbackTraverser : CodeTraverser {

     private ITypeReference typeBeingTraversed;

     private IMetadataHost host;

 

@@ -14,12 +14,12 @@ namespace BytecodeTranslator.Phone {
       this.host = host;

     }

 

-    public override void Visit(ITypeDefinition typeDef) {

+    public override void TraverseChildren(ITypeDefinition typeDef) {

       typeBeingTraversed = typeDef;

-      base.Visit(typeDef);

+      base.TraverseChildren(typeDef);

     }

-    

-    public override void Visit(IMethodCall methodCall) {

+

+    public override void TraverseChildren(IMethodCall methodCall) {

       if (methodCall.MethodToCall.ResolvedMethod.IsSpecialName && methodCall.MethodToCall.Name.Value == "add_BackKeyPress") {

         // check if it is a back key handler and if it is...

         // NAVIGATION TODO this only catches really locally delegate expressions. If it is created before, we see it as a BoundExpression

@@ -91,24 +91,24 @@ namespace BytecodeTranslator.Phone {
           PhoneCodeHelper.instance().BackKeyUnknownDelegateOffenders.Add(typeBeingTraversed);

         }

       }

-      base.Visit(methodCall);

+      base.TraverseChildren(methodCall);

     }

 

     private void parseBlockForNavigation(IBlockStatement block, out bool navigates, out ICollection<string> navTargets) {

       PhoneNavigationCallsTraverser traverser = new PhoneNavigationCallsTraverser(host);

-      traverser.Visit(block);

+      traverser.Traverse(block);

       navigates = traverser.CodeDoesNavigation;

       navTargets = traverser.NavigationTargets;

     }

 

     private void parseBlockForEventCancellation(IBlockStatement block, out bool cancels) {

       PhoneNavigationCallsTraverser traverser = new PhoneNavigationCallsTraverser(host);

-      traverser.Visit(block);

+      traverser.Traverse(block);

       cancels = traverser.CancelsEvents;

     }

   }

 

-  public class PhoneNavigationCallsTraverser : BaseCodeTraverser {

+  public class PhoneNavigationCallsTraverser : CodeTraverser {

     private IMetadataHost host;

 

     public bool CancelsEvents { get; private set; }

@@ -120,7 +120,7 @@ namespace BytecodeTranslator.Phone {
       this.host = host;

     }

 

-    public override void Visit(IMethodCall call) {

+    public override void TraverseChildren(IMethodCall call) {

       checkMethodCallForEventCancellation(call);

       checkMethodCallForNavigation(call);

     }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs
index f3e5ac08..0ed9270c 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs
@@ -6,14 +6,14 @@ using Microsoft.Cci;
 using Microsoft.Cci.MutableCodeModel;

 

 namespace BytecodeTranslator.Phone {

-  class PhoneControlFeedbackCodeTraverser : BaseCodeTraverser {

+  class PhoneControlFeedbackCodeTraverser : CodeTraverser {

     private IMetadataReaderHost host;

 

     public PhoneControlFeedbackCodeTraverser(IMetadataReaderHost host) : base() {

       this.host = host;

     }

 

-    public override void Visit(IMethodCall methodCall) {

+    public override void TraverseChildren(IMethodCall methodCall) {

       if (PhoneCodeHelper.instance().PhoneFeedbackToggled) {

         // check for handlers we do not wish to add feedback checks to

         if (methodCall.MethodToCall.Name.Value.StartsWith("add_")) {

@@ -49,16 +49,16 @@ namespace BytecodeTranslator.Phone {
 

   }

 

-  class PhoneControlFeedbackMetadataTraverser : BaseMetadataTraverser {

+  class PhoneControlFeedbackMetadataTraverser : MetadataTraverser {

     private IMetadataReaderHost host;

 

     public PhoneControlFeedbackMetadataTraverser(IMetadataReaderHost host) : base() {

       this.host = host;

     }

 

-    public override void Visit(IMethodDefinition method) {

+    public override void TraverseChildren(IMethodDefinition method) {

       PhoneControlFeedbackCodeTraverser codeTraverser = new PhoneControlFeedbackCodeTraverser(host);

-      codeTraverser.Visit(method);

+      codeTraverser.TraverseChildren(method);

     }

   }

 }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
index 391aaaaa..db1aac4c 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
@@ -23,7 +23,7 @@ namespace BytecodeTranslator.Phone {
   /// <summary>

   /// Traverse code looking for phone specific points of interest, possibly injecting necessary code in-between

   /// </summary>

-  public class PhoneInitializationCodeTraverser : BaseCodeTraverser {

+  public class PhoneInitializationCodeTraverser : CodeTraverser {

     private readonly IMethodDefinition methodBeingTraversed;

     private static bool initializationFound= false;

     private MetadataReaderHost host;

@@ -185,7 +185,7 @@ namespace BytecodeTranslator.Phone {
     }

 

     public void injectPhoneControlsCode(BlockStatement block) {

-      this.Visit(block);

+      this.Traverse(block);

     }

 

     private void injectPhoneInitializationCode(BlockStatement block, Statement statementAfter) {

@@ -300,9 +300,9 @@ namespace BytecodeTranslator.Phone {
       return new List<IStatement>();

     }

 

-    public override void Visit(IBlockStatement block) {

+    public override void TraverseChildren(IBlockStatement block) {

       foreach (IStatement statement in block.Statements) {

-        this.Visit(statement);

+        this.Traverse(statement);

         if (initializationFound) {

           injectPhoneInitializationCode(block as BlockStatement, statement as Statement);

           initializationFound = false;

@@ -311,7 +311,7 @@ namespace BytecodeTranslator.Phone {
       }

     }

 

-    public override void Visit(IMethodCall methodCall) {

+    public override void TraverseChildren(IMethodCall methodCall) {

       if (methodCall.IsStaticCall ||

           !methodCall.MethodToCall.ContainingType.ResolvedType.Equals(methodBeingTraversed.Container) ||

           methodCall.MethodToCall.Name.Value != "InitializeComponent" ||

@@ -325,7 +325,7 @@ namespace BytecodeTranslator.Phone {
   /// <summary>

   /// Traverse metadata looking only for PhoneApplicationPage's constructors

   /// </summary>

-  public class PhoneInitializationMetadataTraverser : BaseMetadataTraverser {

+  public class PhoneInitializationMetadataTraverser : MetadataTraverser {

     private MetadataReaderHost host;

 

     public PhoneInitializationMetadataTraverser(MetadataReaderHost host)

@@ -333,30 +333,30 @@ namespace BytecodeTranslator.Phone {
         this.host = host;

     }

 

-    public override void Visit(IModule module) {

-      base.Visit(module);

+    public override void TraverseChildren(IModule module) {

+      base.TraverseChildren(module);

     }

 

-    public override void Visit(IAssembly assembly) {

-      base.Visit(assembly);

+    public override void TraverseChildren(IAssembly assembly) {

+      base.TraverseChildren(assembly);

     }

 

     /// <summary>

     /// Check if the type being defined is a PhoneApplicationPage, uninteresting otherwise

     /// </summary>

     /// 

-    public override void Visit(ITypeDefinition typeDefinition) {

+    public override void TraverseChildren(ITypeDefinition typeDefinition) {

       if (typeDefinition.isPhoneApplicationClass(host)) {

         PhoneCodeHelper.instance().setMainAppTypeReference(typeDefinition);

       } else if (typeDefinition.isPhoneApplicationPageClass(host)) {

-        base.Visit(typeDefinition);

+        base.TraverseChildren(typeDefinition);

       }

     }

 

     /// <summary>

     /// Check if it is traversing a constructor. If so, place necessary code after InitializeComponent() call

     /// </summary>

-    public override void Visit(IMethodDefinition method) {

+    public override void TraverseChildren(IMethodDefinition method) {

       if (!method.IsConstructor)

         return;

 

@@ -370,7 +370,7 @@ namespace BytecodeTranslator.Phone {
 

     public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {

       foreach (var a in assemblies) {

-        a.Dispatch(this);

+        this.Traverse((IAssembly)a);

       }

     }

   }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
index 97935721..1957c2fa 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
@@ -5,7 +5,7 @@ using System.Text;
 using Microsoft.Cci;

 

 namespace BytecodeTranslator.Phone {

-  public class PhoneMethodInliningMetadataTraverser : BaseMetadataTraverser {

+  public class PhoneMethodInliningMetadataTraverser : MetadataTraverser {

     private HashSet<IMethodDefinition> methodsToInline;

     private HashSet<IMethodDefinition> iterMethodsToInline;

     private PhoneCodeHelper phoneHelper;

@@ -23,21 +23,21 @@ namespace BytecodeTranslator.Phone {
       TotalMethodsCount = 0;

     }

 

-    public override void Visit(IEnumerable<IModule> modules) {

-      foreach (IModule module in modules) {

-        assemblyBeingTranslated= module.ContainingAssembly;

-        this.Visit(module);

+    public override void TraverseChildren(IAssembly assembly) {

+      foreach (IModule module in assembly.MemberModules) {

+        assemblyBeingTranslated = module.ContainingAssembly;

+        this.Traverse(module);

       }

       firstPassDone = true;

     }

 

-    public override void Visit(IMethodDefinition method) {

+    public override void TraverseChildren(IMethodDefinition method) {

       if (!firstPassDone)

         TotalMethodsCount++;

 

       if (iterMethodsToInline.Contains(method) || (!firstPassDone && phoneHelper.mustInlineMethod(method))) {

         PhoneMethodInliningCodeTraverser codeTraverser= new PhoneMethodInliningCodeTraverser();

-        codeTraverser.Visit(method);

+        codeTraverser.TraverseChildren(method);

         foreach (IMethodDefinition newMethodDef in codeTraverser.getMethodsFound()) {

           bool isExtern = this.assemblyBeingTranslated != null &&

                           !TypeHelper.GetDefiningUnitReference(newMethodDef.ContainingType).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity);

@@ -62,15 +62,15 @@ namespace BytecodeTranslator.Phone {
     public void findAllMethodsToInline(List<IModule> modules) {

       while (!isFinished()) {

         changedOnLastPass = false;

-        Visit(modules);

+        this.Traverse(modules);

       }

     }

   }

 

-  class PhoneMethodInliningCodeTraverser : BaseCodeTraverser {

+  class PhoneMethodInliningCodeTraverser : CodeTraverser {

     private HashSet<IMethodDefinition> foundMethods = new HashSet<IMethodDefinition>();

 

-    public override void Visit(IMethodCall methodCall) {

+    public override void TraverseChildren(IMethodCall methodCall) {

       foundMethods.Add(methodCall.MethodToCall.ResolvedMethod);

     }

 

diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index a5571efa..0fa4a884 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -7,7 +7,7 @@ using Microsoft.Cci.MutableCodeModel;
 using TranslationPlugins;

 

 namespace BytecodeTranslator.Phone {

-  public class PhoneNavigationCodeTraverser : BaseCodeTraverser {

+  public class PhoneNavigationCodeTraverser : CodeTraverser {

     private MetadataReaderHost host;

     private ITypeReference navigationSvcType;

     private ITypeReference cancelEventArgsType;

@@ -38,12 +38,12 @@ namespace BytecodeTranslator.Phone {
       navigationCallers = new HashSet<IMethodReference>();

     }

 

-    public override void Visit(ITypeDefinition typeDef) {

+    public override void TraverseChildren(ITypeDefinition typeDef) {

       this.typeTraversed = typeDef;

-      base.Visit(typeDef);

+      base.TraverseChildren(typeDef);

     }

 

-    public override void Visit(IMethodDefinition method) {

+    public override void TraverseChildren(IMethodDefinition method) {

       this.methodTraversed = method;

       if (method.IsConstructor && PhoneTypeHelper.isPhoneApplicationClass(typeTraversed, host)) {

         navigationCallers.Add(method);

@@ -77,7 +77,7 @@ namespace BytecodeTranslator.Phone {
           }

         }

       }

-      base.Visit(method);

+      base.TraverseChildren(method);

     }

 

 

@@ -87,14 +87,14 @@ namespace BytecodeTranslator.Phone {
     private StaticURIMode currentStaticMode= StaticURIMode.NOT_STATIC;

     private string unpurifiedFoundURI="";

 

-    public override void Visit(IBlockStatement block) {

+    public override void TraverseChildren(IBlockStatement block) {

       IList<Tuple<IStatement,StaticURIMode,string>> staticNavStmts = new List<Tuple<IStatement,StaticURIMode,string>>();

       IList<IStatement> nonStaticNavStmts = new List<IStatement>();

       foreach (IStatement statement in block.Statements) {

         navCallFound = false;

         navCallIsStatic = false;

         navCallIsBack = false;

-        this.Visit(statement);

+        this.Traverse(statement);

         if (navCallFound) {

           navCallers.Add(methodTraversed);

           if (navCallIsStatic) {

@@ -165,7 +165,7 @@ namespace BytecodeTranslator.Phone {
       return true;

     }

 

-    public override void Visit(IMethodCall methodCall) {

+    public override void TraverseChildren(IMethodCall methodCall) {

       string target;

       if (isNavigationOnBackKeyPressHandler(methodCall, out target)) {

         ICollection<Tuple<IMethodReference,string>> targets;

@@ -316,7 +316,7 @@ namespace BytecodeTranslator.Phone {
   /// <summary>

   /// Traverse metadata looking only for PhoneApplicationPage's constructors

   /// </summary>

-  public class PhoneNavigationMetadataTraverser : BaseMetadataTraverser {

+  public class PhoneNavigationMetadataTraverser : MetadataTraverser {

     private MetadataReaderHost host;

     private ITypeDefinition typeBeingTraversed;

     private PhoneNavigationCodeTraverser codeTraverser;

@@ -326,13 +326,15 @@ namespace BytecodeTranslator.Phone {
       this.host = host;

     }

 

-    public override void Visit(IEnumerable<IAssemblyReference> assemblies) {

-      codeTraverser = new PhoneNavigationCodeTraverser(host, assemblies);

-      base.Visit(assemblies);

+    public override void TraverseChildren(IModule module) {

+      codeTraverser = new PhoneNavigationCodeTraverser(host, module.AssemblyReferences);

+      base.Traverse(module.AssemblyReferences);

+      base.TraverseChildren(module);

     }

 

+

     // TODO can we avoid visiting every type? Are there only a few, identifiable, types that may perform navigation?

-    public override void Visit(ITypeDefinition typeDefinition) {

+    public override void TraverseChildren(ITypeDefinition typeDefinition) {

       typeBeingTraversed = typeDefinition;

       if (typeDefinition.isPhoneApplicationClass(host)) {

         NamespaceTypeDefinition mutableTypeDef = typeDefinition as NamespaceTypeDefinition;

@@ -351,22 +353,22 @@ namespace BytecodeTranslator.Phone {
         }

       }

 

-      codeTraverser.Visit(typeDefinition);

-      base.Visit(typeDefinition);

+      codeTraverser.Traverse(typeDefinition);

+      base.TraverseChildren(typeDefinition);

     }

 

     // TODO same here. Are there specific methods (and ways to identfy those) that can perform navigation?

-    public override void Visit(IMethodDefinition method) {

+    public override void TraverseChildren(IMethodDefinition method) {

       if (PhoneCodeHelper.instance().isBackKeyPressOverride(method)) {

         PhoneCodeHelper.instance().KnownBackKeyHandlers.Add(method);

         PhoneCodeHelper.instance().OnBackKeyPressOverriden = true;

       }

-      base.Visit(method);

+      base.TraverseChildren(method);

     }

 

     public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {

       foreach (var a in assemblies) {

-        a.Dispatch(this);

+        this.Traverse((IAssembly)a);

       }

     }

   }

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index d3994a6c..5b9f0afe 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -210,6 +210,9 @@ namespace BytecodeTranslator {
           pdbReader = new PdbReader(pdbStream, host);

         }

         module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;

+        // The decompiler does not turn calls to Assert/Assume into Code Model nodes

+        module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(module);

+

         host.RegisterAsLatest(module);

         modules.Add(module);

         contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));

@@ -396,7 +399,7 @@ namespace BytecodeTranslator {
         System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);

 

         PhoneBackKeyCallbackTraverser traverser = new PhoneBackKeyCallbackTraverser(sink.host);

-        traverser.Visit(modules);

+        traverser.Traverse(modules);

 

       }

     }

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index faa48773..a550d5cd 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -223,7 +223,7 @@ namespace BytecodeTranslator {
       var key = ((IMethodReference)sig);

       this.declaredMethods.TryGetValue(key, out procAndFormalMap);

       var formalMap = procAndFormalMap.FormalMap;

-      formalMap.TryGetValue(param, out mp);

+      mp = formalMap[param.Index];

       return contractContext ? mp.inParameterCopy : mp.outParameterCopy;

     }

 

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

     public struct ProcedureInfo {

       private Bpl.DeclWithFormals decl;

-      private Dictionary<IParameterDefinition, MethodParameter> formalMap;

+      private MethodParameter[] formalMap; // maps parameter index to formal

       private Bpl.Formal thisVariable;

       private Bpl.Formal returnVariable;

       private Bpl.LocalVariable localExcVariable;

@@ -453,20 +453,20 @@ namespace BytecodeTranslator {
       }

       public ProcedureInfo(

         Bpl.DeclWithFormals decl,

-        Dictionary<IParameterDefinition, MethodParameter> formalMap)

+        MethodParameter[] formalMap)

         : this(decl) {

         this.formalMap = formalMap;

       }

       public ProcedureInfo(

         Bpl.DeclWithFormals decl,

-        Dictionary<IParameterDefinition, MethodParameter> formalMap,

+        MethodParameter[] formalMap,

         Bpl.Formal returnVariable)

         : this(decl, formalMap) {

         this.returnVariable = returnVariable;

       }

       public ProcedureInfo(

         Bpl.DeclWithFormals decl,

-        Dictionary<IParameterDefinition, MethodParameter> formalMap,

+        MethodParameter[] formalMap,

         Bpl.Formal returnVariable,

         Bpl.Formal thisVariable,

         Bpl.LocalVariable localExcVariable,

@@ -482,7 +482,7 @@ namespace BytecodeTranslator {
       }

 

       public Bpl.DeclWithFormals Decl { get { return decl; } }

-      public Dictionary<IParameterDefinition, MethodParameter> FormalMap { get { return formalMap; } }

+      public MethodParameter[] FormalMap { get { return formalMap; } }

       public Bpl.Formal ThisVariable { get { return thisVariable; } }

       public Bpl.Formal ReturnVariable { get { return returnVariable; } }

       public Bpl.LocalVariable LocalExcVariable { get { return localExcVariable; } }

@@ -508,13 +508,13 @@ namespace BytecodeTranslator {
         int in_count = 0;

         int out_count = 0;

         MethodParameter mp;

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

+        var formalMap = new MethodParameter[IteratorHelper.EnumerableCount(method.Parameters)];

         foreach (IParameterDefinition formal in method.Parameters) {

           mp = new MethodParameter(formal, this.CciTypeToBoogie(formal.Type));

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

           if (mp.outParameterCopy != null && formal.IsByReference)

             out_count++;

-          formalMap.Add(formal, mp);

+          formalMap[formal.Index] = mp;

         }

 

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

@@ -560,7 +560,7 @@ namespace BytecodeTranslator {
         if (thisVariable != null)

           invars[i++] = thisVariable;

 

-        foreach (MethodParameter mparam in formalMap.Values) {

+        foreach (MethodParameter mparam in formalMap) {

           if (mparam.inParameterCopy != null) {

             invars[i++] = mparam.inParameterCopy;

           }

@@ -675,7 +675,7 @@ namespace BytecodeTranslator {
             if (!TranslationHelper.IsStruct(p2.Type)) continue;

             if (!TypeHelper.TypesAreEquivalent(p1.Type, p2.Type)) continue;

             var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq,

-              Bpl.Expr.Ident(formalMap[p1].inParameterCopy), Bpl.Expr.Ident(formalMap[p2].inParameterCopy)));

+              Bpl.Expr.Ident(formalMap[p1.Index].inParameterCopy), Bpl.Expr.Ident(formalMap[p2.Index].inParameterCopy)));

             boogiePrecondition.Add(req);

           }

         }

@@ -715,7 +715,7 @@ namespace BytecodeTranslator {
           new Bpl.EnsuresSeq()

           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

-        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());

+        procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);

         this.declaredStructDefaultCtors.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

@@ -759,7 +759,7 @@ namespace BytecodeTranslator {
           new Bpl.EnsuresSeq(ens)

           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

-        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());

+        procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);

         this.declaredStructCopyCtors.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

@@ -820,16 +820,18 @@ namespace BytecodeTranslator {
       return result;

     }

 

-    private static int NumGenericParameters(ITypeReference typeReference) {

-      ITypeDefinition typeDefinition = typeReference.ResolvedType;

-      int numParameters = typeDefinition.GenericParameterCount;

-      INestedTypeDefinition ntd = typeDefinition as INestedTypeDefinition;

-      while (ntd != null) {

-        ITypeDefinition containingType = ntd.ContainingType.ResolvedType;

-        numParameters += containingType.GenericParameterCount;

-        ntd = containingType as INestedTypeDefinition;

+    private static ushort ConsolidatedGenericParameterCount(ITypeReference typeReference) {

+      Contract.Requires(typeReference != null);

+

+      var typeDefinition = typeReference.ResolvedType;

+      var totalNumberOfParameters = typeDefinition.GenericParameterCount;

+      var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;

+      while (nestedTypeDefinition != null) {

+        var containingType = nestedTypeDefinition.ContainingType.ResolvedType;

+        totalNumberOfParameters += containingType.GenericParameterCount;

+        nestedTypeDefinition = containingType as INestedTypeDefinition;

       }

-      return numParameters;

+      return totalNumberOfParameters;

     }

 

     public static ITypeReference GetUninstantiatedGenericType(ITypeReference typeReference) {

@@ -871,30 +873,29 @@ namespace BytecodeTranslator {
     /// <paramref name="type"/> in the Bpl program. I.e., its

     /// value represents the expression "typeof(type)".

     /// </summary>

-    public Bpl.Expr FindOrCreateType(ITypeReference type) {

-      // The Heap has to decide how to represent the field (i.e., its type),

-      // all the Sink cares about is adding a declaration for it.

+    public Bpl.Expr FindOrCreateTypeReference(ITypeReference type) {

+

+      var gtir = type as IGenericTypeInstanceReference;

+      if (gtir != null) {

+        var genericType = FindOrDefineType(gtir.GenericType);

+        var gArgs = new Bpl.ExprSeq();

+        foreach (var a in gtir.GenericArguments) {

+          var a_prime = FindOrCreateTypeReference(a);

+          gArgs.Add(a_prime);

+        }

+        var typeExpression = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(genericType), gArgs);

+      }

 

       IGenericTypeParameter gtp = type as IGenericTypeParameter;

       if (gtp != null) {

-        int index = gtp.Index;

-        var nestedType = gtp.DefiningType as INestedTypeDefinition;

-        while (nestedType != null) {

-          // calculate the consolidated index: the parameter knows only its index

-          // in the type that declares it, not including any outer containing types

-          var containingType = nestedType.ContainingTypeDefinition;

-          index += containingType.GenericParameterCount;

-          nestedType = containingType as INestedTypeDefinition;

-        }

-

-        ProcedureInfo info = FindOrCreateProcedure(methodBeingTranslated);

-        if (methodBeingTranslated.IsStatic) {

-          return Bpl.Expr.Ident(info.TypeParameter(index));

-        }

-        else {

-          Bpl.Expr thisExpr = Bpl.Expr.Ident(this.ThisVariable);

-          return new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(childFunctions[index]), new Bpl.ExprSeq(this.Heap.DynamicType(thisExpr)));

+        Bpl.Variable v;

+        if (!this.declaredTypeVariables.TryGetValue(gtp.InternedKey, out v)) {

+          var loc = Bpl.Token.NoToken;

+          var t = CciTypeToBoogie(gtp);

+          v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, gtp.Name.Value, t));

+          this.declaredTypeVariables.Add(gtp.InternedKey, v);

         }

+        return Bpl.Expr.Ident(v);

       }

 

       IGenericMethodParameter gmp = type as IGenericMethodParameter;

@@ -908,123 +909,103 @@ namespace BytecodeTranslator {
       GetConsolidatedTypeArguments(consolidatedTypeArguments, type);

 

       if (consolidatedTypeArguments.Count > 0) {

-        this.FindOrCreateType(uninstantiatedGenericType);

-        var key = uninstantiatedGenericType.InternedKey;

-        Bpl.Function f = this.declaredTypeFunctions[key];

+        this.FindOrCreateTypeReference(uninstantiatedGenericType);

+        var k = uninstantiatedGenericType.InternedKey;

+        var f2 = this.declaredTypeFunctions[k];

         Bpl.ExprSeq args = new Bpl.ExprSeq();

         foreach (ITypeReference p in consolidatedTypeArguments) {

-          args.Add(FindOrCreateType(p));

+          args.Add(FindOrCreateTypeReference(p));

         }

-        Bpl.Expr naryExpr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), args);

+        Bpl.Expr naryExpr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f2), args);

         return naryExpr;

       }

 

-      int numParameters = NumGenericParameters(type);

+      var  f = FindOrDefineType(type);

+      // BUGBUG: Generics!

+      var fCall = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), new Bpl.ExprSeq());

+      return fCall;

+    }

+

+  

+    /// <summary>

+    /// The Heap has to decide how to represent the type. 

+    /// All the Sink cares about is adding a declaration for it.

+    /// </summary>

+    private Bpl.Function FindOrDefineType(ITypeReference type) {

+

+      Bpl.Function f;

+

+      var key = type.InternedKey;

+      if (this.declaredTypeFunctions.TryGetValue(key, out f))

+        return f;

+

+      var numParameters = ConsolidatedGenericParameterCount(type);

+

+      f = this.Heap.CreateTypeFunction(type, numParameters);

+      this.declaredTypeFunctions.Add(key, f);

+      this.TranslatedProgram.TopLevelDeclarations.Add(f);

+      DeclareParents(type.ResolvedType, f);

+

       bool isExtern = this.assemblyBeingTranslated != null &&

                       !TypeHelper.GetDefiningUnitReference(type).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity);

-

-      if (numParameters > 0) {

-        Bpl.Function f;

-        var key = type.InternedKey;

-        if (!this.declaredTypeFunctions.TryGetValue(key, out f)) {

-          Bpl.VariableSeq vseq = new Bpl.VariableSeq();

-          for (int i = 0; i < numParameters; i++) {

-            vseq.Add(new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "arg" + i, this.Heap.TypeType), true));

-          }

-          f = this.Heap.CreateTypeFunction(type, numParameters);

-          this.declaredTypeFunctions.Add(key, f);

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

-          if (numParameters > childFunctions.Count) {

-            for (int i = childFunctions.Count; i < numParameters; i++) {

-              Bpl.Variable input = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "in", this.Heap.TypeType), true);

-              Bpl.Variable output = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "out", this.Heap.TypeType), false);

-              Bpl.Function g = new Bpl.Function(Bpl.Token.NoToken, "Child" + i, new Bpl.VariableSeq(input), output);

-              TranslatedProgram.TopLevelDeclarations.Add(g);

-              childFunctions.Add(g);

-            }

-          }

-          if (isExtern) {

-            var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);

-            f.Attributes = attrib;

-          }

-          else {

-            Bpl.VariableSeq qvars = new Bpl.VariableSeq();

-            Bpl.ExprSeq exprs = new Bpl.ExprSeq();

-            for (int i = 0; i < numParameters; i++) {

-              Bpl.Variable v = new Bpl.Constant(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "arg" + i, this.Heap.TypeType));

-              qvars.Add(v);

-              exprs.Add(Bpl.Expr.Ident(v));

-            }

-            Bpl.Expr e = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(f), exprs);

-            for (int i = 0; i < numParameters; i++) {

-              Bpl.Expr appl = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(childFunctions[i]), new Bpl.ExprSeq(e));

-              Bpl.Trigger trigger = new Bpl.Trigger(Bpl.Token.NoToken, true, new Bpl.ExprSeq(e));

-              Bpl.Expr qexpr = new Bpl.ForallExpr(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), qvars, null, trigger, Bpl.Expr.Eq(appl, Bpl.Expr.Ident(qvars[i])));

-              TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Axiom(Bpl.Token.NoToken, qexpr));

-            }

-          }

-        }

-        return null;

-      }

-      else {

-        Bpl.Variable t;

-        var key = type.InternedKey;

-        if (!this.declaredTypeConstants.TryGetValue(key, out t)) {

-          //List<ITypeReference> structuralParents;

-          //var parents = GetParents(type.ResolvedType, out structuralParents);

-          //t = this.Heap.CreateTypeVariable(type, parents);

-          t = this.Heap.CreateTypeVariable(type, null);

-          this.declaredTypeConstants.Add(key, t);

-          //foreach (var p in structuralParents) {

-          //  var p_prime = FindOrCreateType(p);

-          //  //var e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Subtype, Bpl.Expr.Ident(t), p_prime);

-          //  var e = new Bpl.NAryExpr(

-          //    Bpl.Token.NoToken,

-          //    new Bpl.FunctionCall(this.Heap.Subtype),

-          //    new Bpl.ExprSeq(Bpl.Expr.Ident(t), p_prime)

-          //    );

-          //  var a = new Bpl.Axiom(Bpl.Token.NoToken, e);

-          //  this.TranslatedProgram.TopLevelDeclarations.Add(a);

-          //}

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

-          DeclareParents(type.ResolvedType, t);

-          if (isExtern) {

-            var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);

-            t.Attributes = attrib;

-          }

-        }

-        return Bpl.Expr.Ident(t);

+      if (isExtern) {

+        var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);

+        f.Attributes = attrib;

       }

+      return f;

     }

 

-    private void DeclareSuperType(Bpl.Variable typeDefinitionAsBplConstant, ITypeReference superType) {

-      var superType_prime = FindOrCreateType(superType);

-      var e = new Bpl.NAryExpr(

-        Bpl.Token.NoToken,

-        new Bpl.FunctionCall(this.Heap.Subtype),

-        new Bpl.ExprSeq(Bpl.Expr.Ident(typeDefinitionAsBplConstant), superType_prime)

-        );

-      var a = new Bpl.Axiom(Bpl.Token.NoToken, e);

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

-      if (!superType.ResolvedType.IsInterface) {

-        var e2 = new Bpl.NAryExpr(

-          Bpl.Token.NoToken,

-          new Bpl.FunctionCall(this.Heap.DisjointSubtree),

-          new Bpl.ExprSeq(Bpl.Expr.Ident(typeDefinitionAsBplConstant), superType_prime)

-          );

-        var a2 = new Bpl.Axiom(Bpl.Token.NoToken, e2);

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

-      }

-    }

-    private void DeclareParents(ITypeDefinition typeDefinition, Bpl.Variable typeDefinitionAsBplConstant) {

+    private void DeclareParents(ITypeDefinition typeDefinition, Bpl.Function typeDefinitionAsBplFunction) {

       foreach (var p in typeDefinition.BaseClasses) {

-        DeclareSuperType(typeDefinitionAsBplConstant, p);

+        DeclareSuperType(typeDefinitionAsBplFunction, p);

       }

       foreach (var j in typeDefinition.Interfaces) {

-        DeclareSuperType(typeDefinitionAsBplConstant, j);

+        DeclareSuperType(typeDefinitionAsBplFunction, j);

       }

       return;

     }

+    private void DeclareSuperType(Bpl.Function typeDefinitionAsBplFunction, ITypeReference superType) {

+      var superType_prime = FindOrCreateTypeReference(superType);

+      var numberOfGenericParameters = typeDefinitionAsBplFunction.InParams.Length;

+

+      var qvars = new Bpl.VariableSeq();

+      var exprs = new Bpl.ExprSeq();

+      for (int i = 0; i < numberOfGenericParameters; i++) {

+        var t = typeDefinitionAsBplFunction.InParams[i];

+        qvars.Add(t);

+        exprs.Add(Bpl.Expr.Ident(t));

+      }

+

+      // G(t,u)

+      var callToG = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs);

+      // Subtype(G(t,u), super)

+      Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, superType_prime));

+      Bpl.Expr disjointSubtree = null;

+      var isDisjoint = !superType.ResolvedType.IsInterface;

+      if (isDisjoint) {

+        // DisjointSubtree(G(t,u), super)

+        disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, superType_prime));

+      }

+

+      if (0 < numberOfGenericParameters) {

+

+        // (forall t : Type, u : Type :: { G(t,u) } Subtype(G(t,u), super))

+        var trigger = new Bpl.Trigger(Bpl.Token.NoToken, true, new Bpl.ExprSeq(callToG));

+        var forall = new Bpl.ForallExpr(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), qvars, null, trigger, subtype);

+        subtype = forall;

+

+        if (isDisjoint) {

+          // (forall t : Type, u : Type :: { G(t,u) } DisjointSubtree(G(t,u), super))

+          disjointSubtree = new Bpl.ForallExpr(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), qvars, null, trigger, disjointSubtree);

+        }

+      }

+

+      this.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Axiom(Bpl.Token.NoToken, subtype));

+      if (isDisjoint) {

+        this.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Axiom(Bpl.Token.NoToken, disjointSubtree));

+      }

+

+    }

 

     private List<Bpl.ConstantParent> GetParents(ITypeDefinition typeDefinition, out List<ITypeReference> structuralParents) {

       var parents = new List<Bpl.ConstantParent>();

@@ -1034,7 +1015,7 @@ namespace BytecodeTranslator {
           structuralParents.Add(p);

         }

         else {

-          var v = (Bpl.IdentifierExpr)FindOrCreateType(p);

+          var v = (Bpl.IdentifierExpr)FindOrCreateTypeReference(p);

           parents.Add(new Bpl.ConstantParent(v, true));

         }

       }

@@ -1043,7 +1024,7 @@ namespace BytecodeTranslator {
           structuralParents.Add(j);

         }

         else {

-          var v = (Bpl.IdentifierExpr)FindOrCreateType(j);

+          var v = (Bpl.IdentifierExpr)FindOrCreateTypeReference(j);

           parents.Add(new Bpl.ConstantParent(v, false));

         }

       }

@@ -1053,7 +1034,7 @@ namespace BytecodeTranslator {
     /// <summary>

     /// The keys to the table are the interned key of the type.

     /// </summary>

-    private Dictionary<uint, Bpl.Variable> declaredTypeConstants = new Dictionary<uint, Bpl.Variable>();

+    private Dictionary<uint, Bpl.Variable> declaredTypeVariables = new Dictionary<uint, Bpl.Variable>();

     private Dictionary<uint, Bpl.Function> declaredTypeFunctions = new Dictionary<uint, Bpl.Function>();

     private List<Bpl.Function> childFunctions = new List<Bpl.Function>();

 

@@ -1160,7 +1141,7 @@ namespace BytecodeTranslator {
       mostNestedTryStatementTraverser = new MostNestedTryStatementTraverser();

       escapingGotoEdges = new Dictionary<ITryCatchFinallyStatement, List<string>>();

       nestedTryCatchFinallyStatements = new List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>>();

-      mostNestedTryStatementTraverser.Visit(method.Body);

+      mostNestedTryStatementTraverser.Traverse(method.Body);

     }

 

     public void BeginAssembly(IAssembly assembly) {

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 15f59a13..7a9340db 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -22,18 +22,18 @@ using BytecodeTranslator.Phone;
 

 namespace BytecodeTranslator

 {

-  public class MostNestedTryStatementTraverser : BaseCodeTraverser {

+  public class MostNestedTryStatementTraverser : CodeTraverser {

     Dictionary<IName, ITryCatchFinallyStatement> mostNestedTryStatement = new Dictionary<IName, ITryCatchFinallyStatement>();

     ITryCatchFinallyStatement currStatement = null;

-    public override void Visit(ILabeledStatement labeledStatement) {

+    public override void TraverseChildren(ILabeledStatement labeledStatement) {

       if (currStatement != null)

         mostNestedTryStatement.Add(labeledStatement.Label, currStatement);

-      base.Visit(labeledStatement);

+      base.TraverseChildren(labeledStatement);

     }

-    public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+    public override void TraverseChildren(ITryCatchFinallyStatement tryCatchFinallyStatement) {

       ITryCatchFinallyStatement savedStatement = currStatement;

       currStatement = tryCatchFinallyStatement;

-      base.Visit(tryCatchFinallyStatement);

+      base.TraverseChildren(tryCatchFinallyStatement);

       currStatement = savedStatement;

     }

     public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {

@@ -43,7 +43,7 @@ namespace BytecodeTranslator
     }

   }

 

-  public class StatementTraverser : BaseCodeTraverser {

+  public class StatementTraverser : CodeTraverser {

 

     public readonly TraverserFactory factory;

 

@@ -64,6 +64,7 @@ namespace BytecodeTranslator
       PdbReader = pdbReader;

       this.contractContext = contractContext;

       this.captureState = sink.Options.captureState;

+      this.PreorderVisitor = new SourceContextEmitter(this);

     }

     #endregion

 

@@ -71,7 +72,7 @@ namespace BytecodeTranslator
 

     Bpl.Expr ExpressionFor(IExpression expression) {

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

-      etrav.Visit(expression);

+      etrav.Traverse(expression);

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

       return etrav.TranslatedExpressions.Pop();

     }

@@ -87,11 +88,54 @@ namespace BytecodeTranslator
         var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);

         newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);

       }

-      this.Visit(methodBody);

+      this.Traverse(methodBody);

       return newTypes;

     }

     #endregion

 

+    #region Helper Classes

+    class SourceContextEmitter : CodeVisitor {

+      StatementTraverser parent;

+      public SourceContextEmitter(StatementTraverser parent) {

+        this.parent = parent;

+      }

+

+      public override void Visit(IStatement statement) {

+        EmitSourceContext(statement);

+        if (this.parent.sink.Options.captureState) {

+          var tok = statement.Token();

+          var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);

+          var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);

+          this.parent.StmtBuilder.Add(

+            new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)

+            );

+        }

+      }

+

+      private void EmitSourceContext(IStatement statement) {

+        if (statement is IEmptyStatement) return;

+        var tok = statement.Token();

+        string fileName = null;

+        int lineNumber = 0;

+        if (this.parent.PdbReader != null) {

+          var slocs = this.parent.PdbReader.GetClosestPrimarySourceLocationsFor(statement.Locations);

+          foreach (var sloc in slocs) {

+            fileName = sloc.Document.Location;

+            lineNumber = sloc.StartLine;

+            break;

+          }

+          if (fileName != null) {

+            var attrib = new Bpl.QKeyValue(tok, "sourceLine", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);

+            attrib = new Bpl.QKeyValue(tok, "sourceFile", new List<object> { fileName }, attrib);

+            this.parent.StmtBuilder.Add(

+              new Bpl.AssertCmd(tok, Bpl.Expr.True, attrib)

+              );

+          }

+        }

+      }

+    }

+    #endregion

+

     //public override void Visit(ISourceMethodBody methodBody) {

     //  var block = methodBody.Block as BlockStatement;

     //  // TODO: Error if cast fails?

@@ -103,50 +147,15 @@ namespace BytecodeTranslator
     //  base.Visit(methodBody);

     //}

 

-    public override void Visit(IBlockStatement block) {

+    public override void TraverseChildren(IBlockStatement block) {

       foreach (var s in block.Statements) {

-        this.Visit(s);

-      }

-    }

-

-    public override void Visit(IStatement statement) {

-      EmitSourceContext(statement);

-      if (this.sink.Options.captureState) {

-        var tok = statement.Token();

-        var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);

-        var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);

-        StmtBuilder.Add(

-          new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)

-          );

-      }

-      base.Visit(statement);

-    }

-

-    private void EmitSourceContext(IStatement statement) {

-      if (statement is IEmptyStatement) return;

-      var tok = statement.Token();

-      string fileName = null;

-      int lineNumber = 0;

-      if (this.PdbReader != null) {

-        var slocs = this.PdbReader.GetClosestPrimarySourceLocationsFor(statement.Locations);

-        foreach (var sloc in slocs) {

-          fileName = sloc.Document.Location;

-          lineNumber = sloc.StartLine;

-          break;

-        }

-        if (fileName != null) {

-          var attrib = new Bpl.QKeyValue(tok, "sourceLine", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);

-          attrib = new Bpl.QKeyValue(tok, "sourceFile", new List<object> { fileName }, attrib);

-          StmtBuilder.Add(

-            new Bpl.AssertCmd(tok, Bpl.Expr.True, attrib)

-            );

-        }

+        this.Traverse(s);

       }

     }

 

     #region Basic Statements

 

-    public override void Visit(IAssertStatement assertStatement) {

+    public override void TraverseChildren(IAssertStatement assertStatement) {

       Bpl.Expr conditionExpr = ExpressionFor(assertStatement.Condition);

       Bpl.Type conditionType = this.sink.CciTypeToBoogie(assertStatement.Condition.Type);

       if (conditionType == this.sink.Heap.RefType) {

@@ -165,7 +174,7 @@ namespace BytecodeTranslator
       }

     }

 

-    public override void Visit(IAssumeStatement assumeStatement) {

+    public override void TraverseChildren(IAssumeStatement assumeStatement) {

       Bpl.Expr conditionExpr = ExpressionFor(assumeStatement.Condition);

       Bpl.Type conditionType = this.sink.CciTypeToBoogie(assumeStatement.Condition.Type);

       if (conditionType == this.sink.Heap.RefType) {

@@ -185,13 +194,13 @@ namespace BytecodeTranslator
     /// </summary>

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

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

-    public override void Visit(IConditionalStatement conditionalStatement) {

+    public override void TraverseChildren(IConditionalStatement conditionalStatement) {

       StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

       StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

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

-      condTraverser.Visit(conditionalStatement.Condition);

-      thenTraverser.Visit(conditionalStatement.TrueBranch);

-      elseTraverser.Visit(conditionalStatement.FalseBranch);

+      condTraverser.Traverse(conditionalStatement.Condition);

+      thenTraverser.Traverse(conditionalStatement.TrueBranch);

+      elseTraverser.Traverse(conditionalStatement.FalseBranch);

 

       Bpl.Expr conditionExpr = condTraverser.TranslatedExpressions.Pop();

       Bpl.Type conditionType = this.sink.CciTypeToBoogie(conditionalStatement.Condition.Type);

@@ -221,9 +230,9 @@ namespace BytecodeTranslator
     /// </summary>

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

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

-    public override void Visit(IExpressionStatement expressionStatement) {

+    public override void TraverseChildren(IExpressionStatement expressionStatement) {

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

-      etrav.Visit(expressionStatement.Expression);

+      etrav.Traverse(expressionStatement.Expression);

     }

 

     /// <summary>

@@ -231,18 +240,18 @@ namespace BytecodeTranslator
     /// </summary>

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

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

-    public override void Visit(IBreakStatement breakStatement) {

+    public override void TraverseChildren(IBreakStatement breakStatement) {

       throw new TranslationException("Break statements are not handled");

       //StmtBuilder.Add(new Bpl.BreakCmd(breakStatement.Token(), "I dont know"));

     }

 

-    public override void Visit(IContinueStatement continueStatement) {

+    public override void TraverseChildren(IContinueStatement continueStatement) {

       throw new TranslationException("Continue statements are not handled");

     }

 

-    public override void Visit(ISwitchStatement switchStatement) {

+    public override void TraverseChildren(ISwitchStatement switchStatement) {

       var eTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

-      eTraverser.Visit(switchStatement.Expression);

+      eTraverser.Traverse(switchStatement.Expression);

       var conditionExpr = eTraverser.TranslatedExpressions.Pop();

 

       // Can't depend on default case existing or its index in the collection.

@@ -258,7 +267,7 @@ namespace BytecodeTranslator
       Bpl.StmtList defaultStmts = null;

       if (defaultCase != null) {

         var defaultBodyTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

-        defaultBodyTraverser.Visit(defaultCase.Body);

+        defaultBodyTraverser.Traverse(defaultCase.Body);

         defaultStmts = defaultBodyTraverser.StmtBuilder.Collect(defaultCase.Token());

       }

 

@@ -269,12 +278,12 @@ namespace BytecodeTranslator
         var switchCase = switchCases[i];

 

         var scTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

-        scTraverser.Visit(switchCase.Expression);

+        scTraverser.Traverse(switchCase.Expression);

         var scConditionExpr = scTraverser.TranslatedExpressions.Pop();

         var condition = Bpl.Expr.Eq(conditionExpr, scConditionExpr);

 

         var scBodyTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

-        scBodyTraverser.Visit(switchCase.Body);

+        scBodyTraverser.Traverse(switchCase.Body);

 

         ifCmd = new Bpl.IfCmd(switchCase.Token(),

           condition,

@@ -294,7 +303,7 @@ namespace BytecodeTranslator
     /// the default ctor.

     /// Otherwise ignore it.

     /// </summary>

-    public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {

+    public override void TraverseChildren(ILocalDeclarationStatement localDeclarationStatement) {

       var initVal = localDeclarationStatement.InitialValue;

       var typ = localDeclarationStatement.LocalVariable.Type;

       var isStruct = TranslationHelper.IsStruct(typ);

@@ -329,7 +338,7 @@ namespace BytecodeTranslator
       return;

     }

 

-    public override void Visit(IPushStatement pushStatement) {

+    public override void TraverseChildren(IPushStatement pushStatement) {

       var tok = pushStatement.Token();

       var val = pushStatement.ValueToPush;

       var dup = val as IDupValue;

@@ -348,12 +357,12 @@ namespace BytecodeTranslator
     /// </summary>

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

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

-    public override void Visit(IReturnStatement returnStatement) {

+    public override void TraverseChildren(IReturnStatement returnStatement) {

       Bpl.IToken tok = returnStatement.Token();

 

       if (returnStatement.Expression != null) {

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

-        etrav.Visit(returnStatement.Expression);

+        etrav.Traverse(returnStatement.Expression);

 

         if (this.sink.ReturnVariable == null || etrav.TranslatedExpressions.Count < 1) {

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

@@ -380,7 +389,7 @@ namespace BytecodeTranslator
 

     #region Goto and Labels

 

-    public override void Visit(IGotoStatement gotoStatement) {

+    public override void TraverseChildren(IGotoStatement gotoStatement) {

       IName target = gotoStatement.TargetStatement.Label;

       ITryCatchFinallyStatement targetStatement = this.sink.MostNestedTryStatement(target);

       int count = 0;

@@ -406,24 +415,24 @@ namespace BytecodeTranslator
     /// </summary>

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

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

-    public override void Visit(ILabeledStatement labeledStatement) {

+    public override void TraverseChildren(ILabeledStatement labeledStatement) {

       StmtBuilder.AddLabelCmd(labeledStatement.Label.Value);

-      base.Visit(labeledStatement.Statement);

+      base.Traverse(labeledStatement.Statement);

     }

 

     #endregion

 

     #region Looping Statements

 

-    public override void Visit(IWhileDoStatement whileDoStatement) {

+    public override void TraverseChildren(IWhileDoStatement whileDoStatement) {

       throw new TranslationException("WhileDo statements are not handled");

     }

 

-    public override void Visit(IForEachStatement forEachStatement) {

+    public override void TraverseChildren(IForEachStatement forEachStatement) {

       throw new TranslationException("ForEach statements are not handled");

     }

 

-    public override void Visit(IForStatement forStatement) {

+    public override void TraverseChildren(IForStatement forStatement) {

       throw new TranslationException("For statements are not handled");

     }

 

@@ -489,9 +498,9 @@ namespace BytecodeTranslator
       StmtBuilder.Add(ifCmd);

     }

 

-    public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+    public override void TraverseChildren(ITryCatchFinallyStatement tryCatchFinallyStatement) {

       this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InTry));

-      this.Visit(tryCatchFinallyStatement.TryBody);

+      this.Traverse(tryCatchFinallyStatement.TryBody);

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

       StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));

       this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);

@@ -503,13 +512,13 @@ namespace BytecodeTranslator
       List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();

       this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InCatch));

       foreach (ICatchClause catchClause in tryCatchFinallyStatement.CatchClauses) {

-        typeReferences.Insert(0, this.sink.FindOrCreateType(catchClause.ExceptionType));

+        typeReferences.Insert(0, this.sink.FindOrCreateTypeReference(catchClause.ExceptionType));

         StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

         if (catchClause.ExceptionContainer != Dummy.LocalVariable) {

           Bpl.Variable catchClauseVariable = this.sink.FindOrCreateLocalVariable(catchClause.ExceptionContainer);

           catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(catchClauseVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

         }

-        catchTraverser.Visit(catchClause.Body);

+        catchTraverser.Traverse(catchClause.Body);

         catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

         catchTraverser.StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));

         catchStatements.Insert(0, catchTraverser.StmtBuilder.Collect(catchClause.Token()));

@@ -532,7 +541,7 @@ namespace BytecodeTranslator
         Bpl.Variable savedLabelVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedLabelVariable), Bpl.Expr.Ident(this.sink.LabelVariable)));

-        Visit(tryCatchFinallyStatement.FinallyBody);

+        this.Traverse(tryCatchFinallyStatement.FinallyBody);

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(savedExcVariable)));

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Ident(savedLabelVariable)));

         this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);

@@ -543,14 +552,14 @@ namespace BytecodeTranslator
       RaiseException(raiseExpr);

     }

 

-    public override void Visit(IThrowStatement throwStatement) {

+    public override void TraverseChildren(IThrowStatement throwStatement) {

       ExpressionTraverser exceptionTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

-      exceptionTraverser.Visit(throwStatement.Exception);

+      exceptionTraverser.Traverse(throwStatement.Exception);

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), exceptionTraverser.TranslatedExpressions.Pop()));

       RaiseException();

     }

 

-    public override void Visit(IRethrowStatement rethrowStatement) {

+    public override void TraverseChildren(IRethrowStatement rethrowStatement) {

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

       RaiseException();

     }

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 883d0eaf..a744f405 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -15,7 +15,7 @@ using Microsoft.Cci.Contracts;
 using Microsoft.Cci.ILToCodeModel;

 

 using Bpl = Microsoft.Boogie;

-

+using System.Text.RegularExpressions;

 

 namespace BytecodeTranslator {

 

@@ -131,44 +131,25 @@ namespace BytecodeTranslator {
     }

 

     public static string TurnStringIntoValidIdentifier(string s) {

+

+      // Do this specially just to make the resulting string a little bit more readable.

+      // REVIEW: Just let the main replacement take care of it?

       s = s.Replace("[0:,0:]", "2DArray"); // TODO: Do this programmatically to handle arbitrary arity

       s = s.Replace("[0:,0:,0:]", "3DArray");

       s = s.Replace("[0:,0:,0:,0:]", "4DArray");

       s = s.Replace("[0:,0:,0:,0:,0:]", "5DArray");

-      s = s.Replace('!', '$');

-      s = s.Replace('*', '$');

-      s = s.Replace('+', '$');

-      s = s.Replace('(', '$');

-      s = s.Replace(')', '$');

-      s = s.Replace(',', '$');

       s = s.Replace("[]", "array");

-      s = s.Replace('<', '$');

-      s = s.Replace('>', '$');

-      s = s.Replace(':', '$');

-      s = s.Replace(' ', '$');

-      s = s.Replace('{', '$');

-      s = s.Replace('}', '$');

-      s = s.Replace('-', '$');

-      s = s.Replace(' ', '$');

-      s = s.Replace('\t', '$');

-      s = s.Replace('\r', '$');

-      s = s.Replace('\n', '$');

-      s = s.Replace('\b', '$');

-      s = s.Replace('\x1B', '$');

-      s = s.Replace('/', '$');

-      s = s.Replace('\\', '$');

-      s = s.Replace('=', '$');

-      s = s.Replace('@', '$');

-      s = s.Replace(';', '$');

-      s = s.Replace('%', '$');

-      s = s.Replace('&', '$');

-      s = s.Replace('"', '$');

-      s = s.Replace('[', '$');

-      s = s.Replace(']', '$');

-      s = s.Replace('|', '$');

-      s = s.Replace('+', '$');

-      s = s.Replace('±', '$');

-      s = s.Replace('√', '$');

+

+      // The definition of a Boogie identifier is from BoogiePL.atg.

+      // Just negate that to get which characters should be replaced with a dollar sign.

+

+      // letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".

+      // digit = "0123456789".

+      // special = "'~#$^_.?`".

+      // nondigit = letter + special.

+      // ident =  [ '\\' ] nondigit {nondigit | digit}.

+

+      s = Regex.Replace(s, "[^A-Za-z0-9'~#$^_.?`]", "$");

       

       s = GetRidOfSurrogateCharacters(s);

       return s;

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs
index 60f39e03..1ceb7902 100644
--- a/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs
+++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs
@@ -12,7 +12,7 @@ namespace BytecodeTranslator {
     private Sink sink;

     private IDictionary<IUnit, IContractProvider> contractProviders;

     private IDictionary<IUnit, PdbReader> pdbReaders;

-    private MetadataTraverser traverser;

+    private BCTMetadataTraverser traverser;

 

     public BaseTranslator(TraverserFactory factory, Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

       Factory = factory;

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs
index f2932ac0..ffd6fe52 100644
--- a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs
+++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs
@@ -28,7 +28,9 @@ namespace BytecodeTranslator.TranslationPlugins.Translators {
     }

 

     public override void TranslateAssemblies(IEnumerable<Microsoft.Cci.IUnit> assemblies) {

-      traverser.Visit(assemblies);

+      foreach (var a in assemblies) {

+        traverser.Traverse((IAssembly)a);

+      }

     }

   }

 }

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 472cbb0a..bbc2f7f7 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -25,11 +25,11 @@ namespace BytecodeTranslator {
 

     public abstract Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> reader);

 

-    public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,

+    public virtual BCTMetadataTraverser MakeMetadataTraverser(Sink sink,

       IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?

       IDictionary<IUnit, PdbReader> sourceLocationProviders)

     {

-      return new MetadataTraverser(sink, sourceLocationProviders, this);

+      return new BCTMetadataTraverser(sink, sourceLocationProviders, this);

     }

     public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

       return new StatementTraverser(sink, pdbReader, contractContext, this);

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index 83541f7d..d90176a8 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -29,13 +29,13 @@ namespace BytecodeTranslator {
     /// </summary>

     readonly public Dictionary<ITypeReference, List<ITypeReference>> subTypes = new Dictionary<ITypeReference, List<ITypeReference>>();

 

-    public override MetadataTraverser MakeMetadataTraverser(Sink sink,

+    public override BCTMetadataTraverser MakeMetadataTraverser(Sink sink,

       IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?

       IDictionary<IUnit, PdbReader> pdbReaders) {

       return new WholeProgramMetadataSemantics(this, sink, pdbReaders, this);

     }

 

-    public class WholeProgramMetadataSemantics : MetadataTraverser {

+    public class WholeProgramMetadataSemantics : BCTMetadataTraverser {

 

       readonly WholeProgram parent;

       readonly Sink sink;

@@ -53,13 +53,13 @@ namespace BytecodeTranslator {
         var typeRecorder = new RecordSubtypes(this.parent.subTypes);

         foreach (var a in assemblies) {

           this.codeUnderAnalysis.Add(a, true);

-          typeRecorder.Visit(a);

+          typeRecorder.Traverse((IAssembly)a);

         }

         #endregion

         base.TranslateAssemblies(assemblies);

       }

       

-      class RecordSubtypes : BaseMetadataTraverser {

+      class RecordSubtypes : MetadataTraverser {

 

         Dictionary<ITypeReference, List<ITypeReference>> subTypes;

 

@@ -67,14 +67,14 @@ namespace BytecodeTranslator {
           this.subTypes = subTypes;

         }

 

-        public override void Visit(ITypeDefinition typeDefinition) {

+        public override void TraverseChildren(ITypeDefinition typeDefinition) {

           foreach (var baseClass in typeDefinition.BaseClasses) {

             if (!this.subTypes.ContainsKey(baseClass)) {

               this.subTypes[baseClass] = new List<ITypeReference>();

             }

             this.subTypes[baseClass].Add(typeDefinition);

           }

-          base.Visit(typeDefinition);

+          base.TraverseChildren(typeDefinition);

         }

       }

 

@@ -100,24 +100,24 @@ namespace BytecodeTranslator {
         this.subTypes = parent.subTypes;

       }

 

-      public override void Visit(IMethodCall methodCall) {

+      public override void TraverseChildren(IMethodCall methodCall) {

         var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;

 

         bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");

         bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");

         if (isEventAdd || isEventRemove) {

-          base.Visit(methodCall);

+          base.TraverseChildren(methodCall);

           return;

         }

 

         if (!methodCall.IsVirtualCall) {

-          base.Visit(methodCall);

+          base.TraverseChildren(methodCall);

           return;

         }

         var containingType = methodCall.MethodToCall.ContainingType;

         List<ITypeReference> subTypesOfContainingType;

         if (!this.subTypes.TryGetValue(containingType, out subTypesOfContainingType)) {

-          base.Visit(methodCall);

+          base.TraverseChildren(methodCall);

           return;

         }

         Contract.Assert(0 < subTypesOfContainingType.Count);

@@ -125,7 +125,7 @@ namespace BytecodeTranslator {
         Contract.Assert(!resolvedMethod.IsConstructor);

         var overrides = FindOverrides(containingType, resolvedMethod);

         if (0 == overrides.Count) {

-          base.Visit(methodCall);

+          base.TraverseChildren(methodCall);

           return;

         }

 

@@ -163,6 +163,11 @@ namespace BytecodeTranslator {
         foreach (var typeMethodPair in overrides) {

           var t = typeMethodPair.Item1;

           var m = typeMethodPair.Item2;

+          var typeForT = this.sink.FindOrCreateTypeReference(t);

+          if (typeForT == null) {

+            // BUGBUG!! This just silently skips the branch that would dispatch to t's implementation of the method!

+            continue;

+          }

           var thenBranch = new Bpl.StmtListBuilder();

           methodname = TranslationHelper.CreateUniqueMethodName(m); // REVIEW: Shouldn't this be call to FindOrCreateProcedure?

           if (attrib != null)

@@ -173,7 +178,7 @@ namespace BytecodeTranslator {
           ifcmd = new Bpl.IfCmd(token,

             Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

             this.sink.Heap.DynamicType(inexpr[0]),

-            this.sink.FindOrCreateType(t)

+            typeForT

             ),

             thenBranch.Collect(token),

             null,

@@ -183,6 +188,14 @@ namespace BytecodeTranslator {
           elseBranch.Add(ifcmd);

         }

 

+        if (ifcmd == null) {

+          // BUGBUG: then no override made it into the if-statement.

+          // currently that happens when all types are generic.

+          // Should be able to remove this when that is fixed.

+          base.Traverse(methodCall);

+          return;

+        }

+

         this.StmtTraverser.StmtBuilder.Add(ifcmd);

 

         return;

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index b03c319f..155db7c9 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -344,7 +344,7 @@ type Ref;
 

 const unique null: Ref;

 

-type Type;

+type {:datatype} Type;

 

 type Real;

 

@@ -429,13 +429,13 @@ function $DelegateTypeParameters(Delegate) : Type;
 

 var {:thread_local} $Exception: Ref;

 

-const unique RegressionTestInput.RealNumbers$type: Type;

+function {:constructor} T$RegressionTestInput.RealNumbers() : Type;

 

-const {:extern} unique System.Object$type: Type;

+function {:extern} T$System.Object() : Type;

 

-axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.RealNumbers(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.RealNumbers(), T$System.Object());

 

 procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

 

@@ -576,11 +576,11 @@ implementation T$RegressionTestInput.RealNumbers.#cctor()
 

 

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type;

+function {:constructor} T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() : Type;

 

-axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());

 

 const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;

 

@@ -635,11 +635,11 @@ implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor(
 

 

 

-const unique RegressionTestInput.CreateStruct$type: Type;

+function {:constructor} T$RegressionTestInput.CreateStruct() : Type;

 

-axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.CreateStruct(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.CreateStruct(), T$System.Object());

 

 procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);

 

@@ -649,17 +649,17 @@ procedure RegressionTestInput.S.#default_ctor(this: Ref);
 

 

 

-const unique RegressionTestInput.S$type: Type;

+function {:constructor} T$RegressionTestInput.S() : Type;

 

-const {:extern} unique System.ValueType$type: Type;

+function {:extern} T$System.ValueType() : Type;

 

-axiom $Subtype(System.ValueType$type, System.Object$type);

+axiom $Subtype(T$System.ValueType(), T$System.Object());

 

-axiom $DisjointSubtree(System.ValueType$type, System.Object$type);

+axiom $DisjointSubtree(T$System.ValueType(), T$System.Object());

 

-axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type);

+axiom $Subtype(T$RegressionTestInput.S(), T$System.ValueType());

 

-axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);

+axiom $DisjointSubtree(T$RegressionTestInput.S(), T$System.ValueType());

 

 const unique F$RegressionTestInput.S.x: Field;

 

@@ -675,12 +675,12 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

     call $tmp0 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp0);

-    assume $DynamicType($tmp0) == RegressionTestInput.S$type;

+    assume $DynamicType($tmp0) == T$RegressionTestInput.S();

     s := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

     call $tmp1 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp1);

-    assume $DynamicType($tmp1) == RegressionTestInput.S$type;

+    assume $DynamicType($tmp1) == T$RegressionTestInput.S();

     s := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

     assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 0;

@@ -745,11 +745,11 @@ implementation T$RegressionTestInput.CreateStruct.#cctor()
 

 

 

-const unique RegressionTestInput.ClassWithArrayTypes$type: Type;

+function {:constructor} T$RegressionTestInput.ClassWithArrayTypes() : Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());

 

 var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;

 

@@ -920,11 +920,11 @@ implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor()
 

 

 

-function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;

+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T: Type) : Type;

 

-function Child0(in: Type) : Type;

+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));

 

-axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);

+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));

 

 const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: Field;

 

@@ -959,11 +959,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1
 

 

 

-const unique RegressionTestInput.BitwiseOperations$type: Type;

+function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type;

 

-axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.BitwiseOperations(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.BitwiseOperations(), T$System.Object());

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

@@ -1073,21 +1073,21 @@ implementation T$RegressionTestInput.BitwiseOperations.#cctor()
 

 

 

-const unique RegressionTestInput.AsyncAttribute$type: Type;

+function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type;

 

-const {:extern} unique System.Attribute$type: Type;

+function {:extern} T$System.Attribute() : Type;

 

-axiom $Subtype(System.Attribute$type, System.Object$type);

+axiom $Subtype(T$System.Attribute(), T$System.Object());

 

-axiom $DisjointSubtree(System.Attribute$type, System.Object$type);

+axiom $DisjointSubtree(T$System.Attribute(), T$System.Object());

 

-const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type;

+function {:extern} T$System.Runtime.InteropServices._Attribute() : Type;

 

-axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type);

+axiom $Subtype(T$System.Attribute(), T$System.Runtime.InteropServices._Attribute());

 

-axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

+axiom $Subtype(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());

 

-axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

+axiom $DisjointSubtree(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());

 

 procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref);

 

@@ -1123,11 +1123,11 @@ implementation T$RegressionTestInput.AsyncAttribute.#cctor()
 

 

 

-const unique RegressionTestInput.RefParameters$type: Type;

+function {:constructor} T$RegressionTestInput.RefParameters() : Type;

 

-axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.RefParameters(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.RefParameters(), T$System.Object());

 

 procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

 

@@ -1177,11 +1177,11 @@ implementation T$RegressionTestInput.RefParameters.#cctor()
 

 

 

-const unique RegressionTestInput.NestedGeneric$type: Type;

+function {:constructor} T$RegressionTestInput.NestedGeneric() : Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.NestedGeneric(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric(), T$System.Object());

 

 procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref);

 

@@ -1203,11 +1203,11 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
 

 

 

-const unique RegressionTestInput.NestedGeneric.C$type: Type;

+function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());

 

 procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);

 

@@ -1229,9 +1229,11 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
 

 

 

-function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;

+function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Type;

 

-axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);

+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));

+

+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));

 

 procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);

 

@@ -1273,7 +1275,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
     }

     else

     {

-        call $tmp2 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

+        call $tmp2 := System.Activator.CreateInstance``1(T);

         $tmp1 := Box2Box($tmp2);

         if ($Exception != null)

         {

@@ -1340,11 +1342,11 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re
 

 

 

-const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;

+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() : Type;

 

-axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());

 

 const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: Field;

 

@@ -1379,11 +1381,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#
 

 

 

-const unique RegressionTestInput.Class0$type: Type;

+function {:constructor} T$RegressionTestInput.Class0() : Type;

 

-axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.Class0(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.Class0(), T$System.Object());

 

 var F$RegressionTestInput.Class0.StaticInt: int;

 

@@ -1652,11 +1654,11 @@ implementation T$RegressionTestInput.Class0.#cctor()
 

 

 

-const unique RegressionTestInput.ClassWithBoolTypes$type: Type;

+function {:constructor} T$RegressionTestInput.ClassWithBoolTypes() : Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());

 

 var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index e52668d3..1a2ff101 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -330,7 +330,7 @@ type Ref;
 

 const unique null: Ref;

 

-type Type;

+type {:datatype} Type;

 

 type Real;

 

@@ -415,13 +415,13 @@ function $DelegateTypeParameters(Delegate) : Type;
 

 var {:thread_local} $Exception: Ref;

 

-const unique RegressionTestInput.RealNumbers$type: Type;

+function {:constructor} T$RegressionTestInput.RealNumbers() : Type;

 

-const {:extern} unique System.Object$type: Type;

+function {:extern} T$System.Object() : Type;

 

-axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.RealNumbers(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.RealNumbers(), T$System.Object());

 

 procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

 

@@ -562,11 +562,11 @@ implementation T$RegressionTestInput.RealNumbers.#cctor()
 

 

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type;

+function {:constructor} T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() : Type;

 

-axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), T$System.Object());

 

 var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;

 

@@ -621,11 +621,11 @@ implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor(
 

 

 

-const unique RegressionTestInput.CreateStruct$type: Type;

+function {:constructor} T$RegressionTestInput.CreateStruct() : Type;

 

-axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.CreateStruct(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.CreateStruct(), T$System.Object());

 

 procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);

 

@@ -635,17 +635,17 @@ procedure RegressionTestInput.S.#default_ctor(this: Ref);
 

 

 

-const unique RegressionTestInput.S$type: Type;

+function {:constructor} T$RegressionTestInput.S() : Type;

 

-const {:extern} unique System.ValueType$type: Type;

+function {:extern} T$System.ValueType() : Type;

 

-axiom $Subtype(System.ValueType$type, System.Object$type);

+axiom $Subtype(T$System.ValueType(), T$System.Object());

 

-axiom $DisjointSubtree(System.ValueType$type, System.Object$type);

+axiom $DisjointSubtree(T$System.ValueType(), T$System.Object());

 

-axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type);

+axiom $Subtype(T$RegressionTestInput.S(), T$System.ValueType());

 

-axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);

+axiom $DisjointSubtree(T$RegressionTestInput.S(), T$System.ValueType());

 

 var F$RegressionTestInput.S.x: [Ref]int;

 

@@ -661,12 +661,12 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

     call $tmp0 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp0);

-    assume $DynamicType($tmp0) == RegressionTestInput.S$type;

+    assume $DynamicType($tmp0) == T$RegressionTestInput.S();

     s := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

     call $tmp1 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp1);

-    assume $DynamicType($tmp1) == RegressionTestInput.S$type;

+    assume $DynamicType($tmp1) == T$RegressionTestInput.S();

     s := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

     assert F$RegressionTestInput.S.x[s] == 0;

@@ -731,11 +731,11 @@ implementation T$RegressionTestInput.CreateStruct.#cctor()
 

 

 

-const unique RegressionTestInput.ClassWithArrayTypes$type: Type;

+function {:constructor} T$RegressionTestInput.ClassWithArrayTypes() : Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithArrayTypes(), T$System.Object());

 

 var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;

 

@@ -906,11 +906,11 @@ implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor()
 

 

 

-function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;

+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T: Type) : Type;

 

-function Child0(in: Type) : Type;

+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));

 

-axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);

+axiom (forall T: Type :: { T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) } $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), T$System.Object()));

 

 var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: [Ref]int;

 

@@ -945,11 +945,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1
 

 

 

-const unique RegressionTestInput.BitwiseOperations$type: Type;

+function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type;

 

-axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.BitwiseOperations(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.BitwiseOperations(), T$System.Object());

 

 procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

@@ -1059,21 +1059,21 @@ implementation T$RegressionTestInput.BitwiseOperations.#cctor()
 

 

 

-const unique RegressionTestInput.AsyncAttribute$type: Type;

+function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type;

 

-const {:extern} unique System.Attribute$type: Type;

+function {:extern} T$System.Attribute() : Type;

 

-axiom $Subtype(System.Attribute$type, System.Object$type);

+axiom $Subtype(T$System.Attribute(), T$System.Object());

 

-axiom $DisjointSubtree(System.Attribute$type, System.Object$type);

+axiom $DisjointSubtree(T$System.Attribute(), T$System.Object());

 

-const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type;

+function {:extern} T$System.Runtime.InteropServices._Attribute() : Type;

 

-axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type);

+axiom $Subtype(T$System.Attribute(), T$System.Runtime.InteropServices._Attribute());

 

-axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

+axiom $Subtype(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());

 

-axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

+axiom $DisjointSubtree(T$RegressionTestInput.AsyncAttribute(), T$System.Attribute());

 

 procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref);

 

@@ -1109,11 +1109,11 @@ implementation T$RegressionTestInput.AsyncAttribute.#cctor()
 

 

 

-const unique RegressionTestInput.RefParameters$type: Type;

+function {:constructor} T$RegressionTestInput.RefParameters() : Type;

 

-axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.RefParameters(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.RefParameters(), T$System.Object());

 

 procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

 

@@ -1163,11 +1163,11 @@ implementation T$RegressionTestInput.RefParameters.#cctor()
 

 

 

-const unique RegressionTestInput.NestedGeneric$type: Type;

+function {:constructor} T$RegressionTestInput.NestedGeneric() : Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.NestedGeneric(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric(), T$System.Object());

 

 procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref);

 

@@ -1189,11 +1189,11 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
 

 

 

-const unique RegressionTestInput.NestedGeneric.C$type: Type;

+function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C(), T$System.Object());

 

 procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);

 

@@ -1215,9 +1215,11 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
 

 

 

-function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;

+function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Type;

 

-axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);

+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));

+

+axiom (forall T: Type :: { T$RegressionTestInput.NestedGeneric.C.G`1(T) } $DisjointSubtree(T$RegressionTestInput.NestedGeneric.C.G`1(T), T$System.Object()));

 

 procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);

 

@@ -1259,7 +1261,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
     }

     else

     {

-        call $tmp2 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

+        call $tmp2 := System.Activator.CreateInstance``1(T);

         $tmp1 := Box2Box($tmp2);

         if ($Exception != null)

         {

@@ -1326,11 +1328,11 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re
 

 

 

-const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;

+function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() : Type;

 

-axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), T$System.Object());

 

 var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;

 

@@ -1365,11 +1367,11 @@ implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#
 

 

 

-const unique RegressionTestInput.Class0$type: Type;

+function {:constructor} T$RegressionTestInput.Class0() : Type;

 

-axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.Class0(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.Class0(), T$System.Object());

 

 var F$RegressionTestInput.Class0.StaticInt: int;

 

@@ -1638,11 +1640,11 @@ implementation T$RegressionTestInput.Class0.#cctor()
 

 

 

-const unique RegressionTestInput.ClassWithBoolTypes$type: Type;

+function {:constructor} T$RegressionTestInput.ClassWithBoolTypes() : Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

+axiom $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

+axiom $DisjointSubtree(T$RegressionTestInput.ClassWithBoolTypes(), T$System.Object());

 

 var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;