merge

1 files changed, 3 insertions, 25 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 7eacf697..12a6084f 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -37,13 +37,13 @@ namespace Microsoft.Boogie {
         goto END;

       }

       if (CommandLineOptions.Clo.Files.Count == 0) {

-        ExecutionEngine.printer.ErrorWriteLine("*** Error: No input files were specified.");

+        ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified.");

         goto END;

       }

       if (CommandLineOptions.Clo.XmlSink != null) {

         string errMsg = CommandLineOptions.Clo.XmlSink.Open();

         if (errMsg != null) {

-          ExecutionEngine.printer.ErrorWriteLine("*** Error: " + errMsg);

+          ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg);

           goto END;

         }

       }

@@ -84,7 +84,7 @@ namespace Microsoft.Boogie {
           extension = extension.ToLower();

         }

         if (extension != ".bpl") {

-          ExecutionEngine.printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

+          ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

               extension == null ? "" : extension);

           goto END;

         }

@@ -100,27 +100,5 @@ namespace Microsoft.Boogie {
         Console.ReadLine();

       }

     }

-    

-

-    #region // TODO: Is this still used?

-

-    enum FileType

-    {

-      Unknown,

-      Cil,

-      Bpl,

-      Dafny

-    };

-

-

-    static bool ProgramHasDebugInfo(Program program)

-    {

-      Contract.Requires(program != null);

-      // We inspect the last declaration because the first comes from the prelude and therefore always has source context.

-      return program.TopLevelDeclarations.Count > 0 &&

-          ((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);

-    }

-

-    #endregion

   }

 }