Merge

19 files changed, 519 insertions, 501 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;

 

diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl
index 26ffd337..2bca4e83 100644
--- a/Test/datatypes/t2.bpl
+++ b/Test/datatypes/t2.bpl
@@ -1,36 +1,54 @@
 

 type {:datatype} DotNetType;

 

+/*\

+ *  Subtype Axioms

+\*/

+function $Subtype(DotNetType, DotNetType) : bool;

+// reflexive

+axiom (forall t: DotNetType :: $Subtype(t, t));

+// anti-symmetric

+axiom (forall t0: DotNetType, t1: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t0) } $Subtype(t0, t1) && $Subtype(t1, t0) ==> t0 == t1);

+// transitive

+axiom (forall t0: DotNetType, t1: DotNetType, t2: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t2) } $Subtype(t0, t1) && $Subtype(t1, t2) ==> $Subtype(t0, t2));

+

+/*\

+ *  Type Declarations

+\*/

 // class System.Object { ... }

 function {:constructor} System.Object() : DotNetType;

 

-// class NominalType2 : System.Object { ... }

-function {:constructor} NominalType2() : DotNetType;

-axiom $Subtype(NominalType2(), System.Object());

+// class B : System.Object { ... }

+function {:constructor} B() : DotNetType;

+axiom $Subtype(B(), System.Object());

 

 // class GenericType1<T> : System.Object { ... }

 function {:constructor} GenericType1(T:DotNetType) : DotNetType;

 axiom (forall t : DotNetType :: $Subtype(GenericType1(t), System.Object()));

 

-function $Subtype(DotNetType, DotNetType) : bool;

-// reflexive

-axiom (forall t: DotNetType :: $Subtype(t, t));

-// anti-symmetric

-axiom (forall t0: DotNetType, t1: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t0) } $Subtype(t0, t1) && $Subtype(t1, t0) ==> t0 == t1);

-// transitive

-axiom (forall t0: DotNetType, t1: DotNetType, t2: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t2) } $Subtype(t0, t1) && $Subtype(t1, t2) ==> $Subtype(t0, t2));

+// class C : GenericType1<object>

+function {:constructor} C() : DotNetType;

+axiom $Subtype(C(), GenericType1(System.Object()));

+

+// class D<U> : GenericType1<U>

+function {:constructor} D(U:DotNetType) : DotNetType;

+axiom (forall u : DotNetType :: $Subtype(D(u), GenericType1(u)));

+

+// class GenericType2<T,U> : System.Object { ... }

+function {:constructor} GenericType2(T:DotNetType, U:DotNetType) : DotNetType;

+axiom (forall t : DotNetType, u : DotNetType :: $Subtype(GenericType2(t,u), System.Object()));

 

 procedure foo(t : DotNetType) 

 {

   assert System.Object() != GenericType1(t);

-  assert System.Object() != NominalType2();

+  assert System.Object() != B();

 }

 

 procedure bar(t : DotNetType, u : DotNetType) 

   requires t != u;

 {

   assert System.Object() != GenericType1(t);

-  assert System.Object() != NominalType2();

+  assert System.Object() != B();

   assert GenericType1(t) != GenericType1(u);

 }