Moved the creation of Boogie procedures from the MetadataTraverser to the Sink because a procedure needs to be created for every method called in the translated program and not just the methods defined in the assembly being translated. This means the contract provider is needed only in the sink and not by any of the traversers.

1 files changed, 1 insertions, 1 deletions

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 6efe04e2..8162af9e 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -20,7 +20,7 @@ namespace BytecodeTranslator {
   public abstract class TraverserFactory {

     public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, PdbReader/*?*/ pdbReader, HeapFactory heapFactory)

     {

-      return new MetadataTraverser(new Sink(this, heapFactory), contractProvider, pdbReader);

+      return new MetadataTraverser(new Sink(this, heapFactory, contractProvider), pdbReader);

     }

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

       return new StatementTraverser(sink, pdbReader);