diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 53 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 3 |
2 files changed, 1 insertions, 55 deletions
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);
}
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 6a974694..ed28d4de 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -3,11 +3,8 @@ using System.Collections.Generic; using System.Diagnostics.Contracts;
using Microsoft.Boogie;
using VC;
-// Here come the Dafny/Boogie specific imports
-//using PureCollections;
using Bpl = Microsoft.Boogie;
using Dafny = Microsoft.Dafny;
-// using AI = Microsoft.AbstractInterpretationFramework;
namespace DafnyLanguage
|