Add an option to allow automatically generated requirements to be printed

to a file, making them easier to inspect and manipulate.

1 files changed, 11 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index b198e224..aa275ade 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -42,6 +42,7 @@ namespace Microsoft.Dafny
     public bool SpillTargetCode = false;

     public bool DisallowIncludes = false;

     public bool DisableNLarith = false;

+    public string AutoReqPrintFile = null;

 

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

       var args = ps.args;  // convenient synonym

@@ -109,6 +110,12 @@ namespace Microsoft.Dafny
           this.Z3Options.Add("NL_ARITH=false");

           return true;

 

+        case "autoReqPrint":

+          if (ps.ConfirmArgumentCount(1)) {

+              AutoReqPrintFile = args[ps.i];

+          }

+          return true;

+

         default:

           break;

       }

@@ -174,6 +181,10 @@ namespace Microsoft.Dafny
                     how discriminating they are:  0 < 1 < 2 < (3,4) < 5 < 6

                 6 (default) - most discriminating

   /noIncludes   Ignore include directives

+  /noNLarith    Reduce Z3's knowledge of non-linear arithmetic (*,/,%). 

+                Results in more manual work, but also produces more predictable behavior.

+  /autoReqPrint:<file>

+                Print out requirements that were automatically generated by autoReq.

 ");

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

     }