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

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

1 files changed, 4 insertions, 1 deletions

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);

 

       }

     }