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/DafnyDriver | |
| parent | 5f5f709c8f3924ddbfbb48f52b7875eac143503a (diff) | |
Add support for counting spec/impl/proof lines by supressing, e.g., ghost statements
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 99d4938e..8046a7ac 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -147,7 +147,8 @@ namespace Microsoft.Dafny if (err != null) {
exitValue = ExitValue.DAFNY_ERROR;
printer.ErrorWriteLine(Console.Out, err);
- } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck) {
+ } else if (dafnyProgram != null && !CommandLineOptions.Clo.NoResolve && !CommandLineOptions.Clo.NoTypecheck
+ && DafnyOptions.O.DafnyVerify) {
Dafny.Translator translator = new Dafny.Translator();
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
if (CommandLineOptions.Clo.PrintFile != null)
|