diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-10-27 14:13:17 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-10-27 14:13:17 -0700 |
| commit | 715b21620d5e810b03a2f7cdeb2d8d7070bd70ef (patch) | |
| tree | ef02d2facd364ed595c7e4fbc5c3d99f72a6d210 /Source/Dafny/DafnyMain.cs | |
| parent | 5f5f709c8f3924ddbfbb48f52b7875eac143503a (diff) | |
Add support for counting spec/impl/proof lines by supressing, e.g., ghost statements
Diffstat (limited to 'Source/Dafny/DafnyMain.cs')
| -rw-r--r-- | Source/Dafny/DafnyMain.cs | 42 |
1 files changed, 18 insertions, 24 deletions
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs index 60578e33..34b509a0 100644 --- a/Source/Dafny/DafnyMain.cs +++ b/Source/Dafny/DafnyMain.cs @@ -11,6 +11,21 @@ using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny {
public class Main {
+
+ private static void MaybePrintProgram(Program program, string filename)
+ {
+ if (filename != null) {
+ TextWriter tw;
+ if (filename == "-") {
+ tw = System.Console.Out;
+ } else {
+ tw = new System.IO.StreamWriter(filename);
+ }
+ Printer pr = new Printer(tw, DafnyOptions.O.PrintMode);
+ pr.PrintProgram(program);
+ }
+ }
+
/// <summary>
/// Returns null on success, or an error string otherwise.
/// </summary>
@@ -47,35 +62,14 @@ namespace Microsoft.Dafny { 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);
- }
- }
- }
+ MaybePrintProgram(program, DafnyOptions.O.DafnyPrintFile);
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);
- }
- }
- }
+ MaybePrintProgram(program, DafnyOptions.O.DafnyPrintResolvedFile);
+
if (r.ErrorCount != 0) {
return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, program.Name);
}
|