Add support for counting spec/impl/proof lines by supressing, e.g., ghost statements

1 files changed, 46 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index aa275ade..f9146cca 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -35,6 +35,9 @@ namespace Microsoft.Dafny
     public int InductionHeuristic = 6;

     public string DafnyPrelude = null;

     public string DafnyPrintFile = null;

+    public enum PrintModes { Everything, NoIncludes, NoGhost };

+    public PrintModes PrintMode;

+    public bool DafnyVerify = true;

     public string DafnyPrintResolvedFile = null;

     public bool Compile = true;

     public bool ForceCompile = false;

@@ -43,6 +46,7 @@ namespace Microsoft.Dafny
     public bool DisallowIncludes = false;

     public bool DisableNLarith = false;

     public string AutoReqPrintFile = null;

+    public bool ignoreAutoReq = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -60,6 +64,26 @@ namespace Microsoft.Dafny
           }

           return true;

 

+        case "printMode":

+          if (ps.ConfirmArgumentCount(1)) {

+            if (args[ps.i].Equals("Everything")) {

+              PrintMode = PrintModes.Everything;

+            }

+            else if (args[ps.i].Equals("NoIncludes"))

+            {

+                PrintMode = PrintModes.NoIncludes;

+            }

+            else if (args[ps.i].Equals("NoGhost"))

+            {

+                PrintMode = PrintModes.NoGhost;

+            }

+            else

+            {

+                throw new Exception("Invalid value for printMode");

+            }

+          }

+          return true;

+

         case "rprint":

           if (ps.ConfirmArgumentCount(1)) {

             DafnyPrintResolvedFile = args[ps.i];

@@ -77,6 +101,15 @@ namespace Microsoft.Dafny
             return true;

           }

 

+        case "dafnyVerify":

+            {

+                int verify = 0;

+                if (ps.GetNumericArgument(ref verify, 2)) {

+                    DafnyVerify = verify != 0; // convert to boolean

+                }

+                return true;

+            }

+

         case "spillTargetCode": {

             int spill = 0;

             if (ps.GetNumericArgument(ref spill, 2)) {

@@ -116,6 +149,10 @@ namespace Microsoft.Dafny
           }

           return true;

 

+        case "noAutoReq":

+          ignoreAutoReq = true;

+          return true;

+

         default:

           break;

       }

@@ -146,9 +183,17 @@ namespace Microsoft.Dafny
   /dprint:<file>

                 print Dafny program after parsing it

                 (use - as <file> to print to console)

+  /printMode:<Everything|NoIncludes|NoGhost>

+                NoIncludes disables printing of {:verify false} methods incorporated via the

+                include mechanism, as well as datatypes and fields included from other files.

+                NoGhost disables printing of functions, ghost methods, and proof statements in

+                implementation methods.  It also disables anything NoIncludes disables.

   /rprint:<file>

                 print Dafny program after resolving it

                 (use - as <file> to print to console)

+  /dafnyVerify:<n>

+                0 - stop after typechecking

+                1 - continue on to translation, verification, and compilation

   /compile:<n>  0 - do not compile Dafny program

                 1 (default) - upon successful verification of the Dafny

                     program, compile Dafny program to .NET assembly

@@ -185,6 +230,7 @@ namespace Microsoft.Dafny
                 Results in more manual work, but also produces more predictable behavior.

   /autoReqPrint:<file>

                 Print out requirements that were automatically generated by autoReq.

+  /noAutoReq    Ignore autoReq attributes

 ");

       base.Usage();  // also print the Boogie options

     }