diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
| commit | 8911e5c95d4715c2e2626aef67f19793d6f43201 (patch) | |
| tree | d703bfd931802e780430e32f1339cf77adc342a4 /Source/Dafny/DafnyMain.cs | |
| parent | 1c375d1889e628fcd2a1a0fc041673a5f4230d84 (diff) | |
Put all sources under \Source directory
Diffstat (limited to 'Source/Dafny/DafnyMain.cs')
| -rw-r--r-- | Source/Dafny/DafnyMain.cs | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs new file mode 100644 index 00000000..6091e522 --- /dev/null +++ b/Source/Dafny/DafnyMain.cs @@ -0,0 +1,88 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Bpl = Microsoft.Boogie;
+
+namespace Microsoft.Dafny {
+ public class Main {
+ /// <summary>
+ /// Returns null on success, or an error string otherwise.
+ /// </summary>
+ public static string ParseCheck(List<string/*!*/>/*!*/ fileNames, string/*!*/ programName, out Program program)
+ //modifies Bpl.CommandLineOptions.Clo.XmlSink.*;
+ {
+ Contract.Requires(programName != null);
+ Contract.Requires(fileNames != null);
+ program = null;
+ ModuleDecl module = new LiteralModuleDecl(new DefaultModuleDecl(), null);
+ BuiltIns builtIns = new BuiltIns();
+ foreach (string dafnyFileName in fileNames){
+ Contract.Assert(dafnyFileName != null);
+ if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
+ Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);
+ }
+ if (Bpl.CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("Parsing " + dafnyFileName);
+ }
+
+ int errorCount;
+ try
+ {
+ errorCount = Dafny.Parser.Parse(dafnyFileName, module, builtIns);
+ if (errorCount != 0)
+ {
+ return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);
+ }
+ }
+ catch (IOException e)
+ {
+ return string.Format("Error opening file \"{0}\": {1}", dafnyFileName, e.Message);
+ }
+ }
+
+ program = new Program(programName, module, builtIns);
+
+ if (DafnyOptions.O.DafnyPrintFile != null) {
+ string filename = DafnyOptions.O.DafnyPrintFile;
+ if (filename == "-") {
+ Printer pr = new Printer(System.Console.Out);
+ pr.PrintProgram(program);
+ } else {
+ using (TextWriter writer = new System.IO.StreamWriter(filename)) {
+ Printer pr = new Printer(writer);
+ pr.PrintProgram(program);
+ }
+ }
+ }
+
+ if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
+
+ Dafny.Resolver r = new Dafny.Resolver(program);
+ r.ResolveProgram(program);
+ if (DafnyOptions.O.DafnyPrintResolvedFile != null) {
+ string filename = DafnyOptions.O.DafnyPrintResolvedFile;
+ if (filename == "-") {
+ Printer pr = new Printer(System.Console.Out);
+ pr.PrintProgram(program);
+ } else {
+ using (TextWriter writer = new System.IO.StreamWriter(filename)) {
+ Printer pr = new Printer(writer);
+ pr.PrintProgram(program);
+ }
+ }
+ }
+ if (r.ErrorCount != 0) {
+ return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, programName);
+ }
+
+ return null; // success
+ }
+ }
+}
|