1 files changed, 36 insertions, 11 deletions
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index c8300189..c6d8e7a4 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -168,18 +168,46 @@ namespace BytecodeTranslator {
           return 1;
         }
 
-        result = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList);
+        var pgm = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList);
+        var fileName = assemblyNames[0];
+        fileName = Path.GetFileNameWithoutExtension(fileName);
+        string outputFileName = fileName + ".bpl";
+        Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
+        Prelude.Emit(writer);
+        pgm.Emit(writer);
+        writer.Close();
+        return 0; // success
 
       } catch (Exception e) { // swallow everything and just return an error code
         Console.WriteLine("The byte-code translator failed: {0}", e.Message);
         // Console.WriteLine("Stack trace: {0}", e.StackTrace);
         return -1;
       }
-      return result;
     }
 
     private static List<IModule> modules;
-    public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
+
+    public static int TranslateAssemblyAndWriteOutput(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
+      Contract.Requires(assemblyNames != null);
+      Contract.Requires(heapFactory != null);
+      try {
+        var pgm = TranslateAssembly(assemblyNames, heapFactory, options, exemptionList, whiteList);
+        var fileName = assemblyNames[0];
+        fileName = Path.GetFileNameWithoutExtension(fileName);
+        string outputFileName = fileName + ".bpl";
+        Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
+        Prelude.Emit(writer);
+        pgm.Emit(writer);
+        writer.Close();
+        return 0; // success
+      } catch (Exception e) { // swallow everything and just return an error code
+        Console.WriteLine("The byte-code translator failed: {0}", e.Message);
+        // Console.WriteLine("Stack trace: {0}", e.StackTrace);
+        return -1;
+      }
+    }
+
+    public static Bpl.Program/*?*/ TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
       Contract.Requires(assemblyNames != null);
       Contract.Requires(heapFactory != null);
 
@@ -193,6 +221,8 @@ namespace BytecodeTranslator {
       var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
       Host = host;
 
+      Bpl.CommandLineOptions.Install(new Bpl.CommandLineOptions());
+
       #region Assemlies to translate (via cmd line)
       modules = new List<IModule>();
       var contractExtractors = new Dictionary<IUnit, IContractProvider>();
@@ -266,8 +296,7 @@ namespace BytecodeTranslator {
       #endregion
 
       if (modules.Count == 0) {
-        Console.WriteLine("No input assemblies to translate.");
-        return -1;
+        throw new TranslationException("No input assemblies to translate.");
       }
 
       var primaryModule = modules[0];
@@ -378,14 +407,10 @@ namespace BytecodeTranslator {
       //  }
       //}
       //sink.TranslatedProgram.TopLevelDeclarations = goodDecls;
-
-      Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
-      Prelude.Emit(writer);
-      sink.TranslatedProgram.Emit(writer);
-      writer.Close();
-      return 0; // success
+      return sink.TranslatedProgram;
     }
 
+
     private static void finalizeNavigationAnalysisAndBoogieCode(string phoneControlsConfigFile, Sink sink, string outputFileName) {
       outputBoogieTrackedControlConfiguration(phoneControlsConfigFile);
       checkTransitivelyCalledBackKeyNavigations(modules);