From e2668d447fb277cd11e114579c1a27de185aaec0 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 3 Jun 2013 17:34:00 -0700
Subject: Did some refactoring of the Dafny drivers.

---
 Source/DafnyDriver/DafnyDriver.cs | 53 +--------------------------------------
 1 file changed, 1 insertion(+), 52 deletions(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index e3bea140..152e43bb 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -145,57 +145,6 @@ namespace Microsoft.Dafny
     }
 
 
-    // TODO(wuestholz): Use the definition in the Boogie driver.
-    /// <summary>
-    /// Parse the given files into one Boogie program.  If an I/O or parse error occurs, an error will be printed
-    /// and null will be returned.  On success, a non-null program is returned.
-    /// </summary>
-    static Bpl.Program ParseBoogieProgram(List<string/*!*/>/*!*/ fileNames, bool suppressTraceOutput)
-    {
-      Contract.Requires(cce.NonNullElements(fileNames));
-      //BoogiePL.Errors.count = 0;
-      Bpl.Program program = null;
-      bool okay = true;
-      foreach (string bplFileName in fileNames) {
-        if (!suppressTraceOutput) {
-          if (CommandLineOptions.Clo.XmlSink != null) {
-            CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName);
-          }
-          if (CommandLineOptions.Clo.Trace) {
-            Console.WriteLine("Parsing " + bplFileName);
-          }
-        }
-
-        Bpl.Program programSnippet;
-        int errorCount;
-        try {
-          errorCount = Microsoft.Boogie.Parser.Parse(bplFileName, (List<string>)null, out programSnippet);
-          if (programSnippet == null || errorCount != 0) {
-            Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
-            okay = false;
-            continue;
-          }
-        } catch (IOException e) {
-          printer.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
-          okay = false;
-          continue;
-        }
-        if (program == null) {
-          program = programSnippet;
-        } else if (programSnippet != null) {
-          program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations);
-        }
-      }
-      if (!okay) {
-        return null;
-      } else if (program == null) {
-        return new Bpl.Program();
-      } else {
-        return program;
-      }
-    }
-
-
     /// <summary>
     /// Resolve, type check, infer invariants for, and verify the given Boogie program.
     /// The intention is that this Boogie program has been produced by translation from something
@@ -227,7 +176,7 @@ namespace Microsoft.Dafny
 
             List<string/*!*/>/*!*/ fileNames = new List<string/*!*/>();
             fileNames.Add(bplFileName);
-            Bpl.Program reparsedProgram = ParseBoogieProgram(fileNames, true);
+            Bpl.Program reparsedProgram = ExecutionEngine.ParseBoogieProgram(fileNames, true);
             if (reparsedProgram != null) {
               ResolveAndTypecheck(reparsedProgram, bplFileName);
             }
-- 
cgit v1.2.3