Simplified the translator by merging the ToplevelTraverser, ClassTraverser, and MethodTraverser into one traverser: MetadataTraverser. It will have to do a little more work to keep its state consistent (like saving any type-related state before traversing a nested type definition), but it seems worth it.

1 files changed, 2 insertions, 4 deletions

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

 namespace BytecodeTranslator {

   public abstract class TraverserFactory {

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

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

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

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

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

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

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

   }

 }
\ No newline at end of file