Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero.

The test suite relies on error codes all being zero (except for preprocessing
errors), so add a flag for that (as suggested in a source comment).

1 files changed, 15 insertions, 1 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 4fc2de96..a6827d5f 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -54,6 +54,7 @@ namespace Microsoft.Dafny
     public string AutoReqPrintFile = null;

     public bool ignoreAutoReq = false;

     public bool AllowGlobals = false;

+    public bool CountVerificationErrors = true;

 

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

       var args = ps.args;  // convenient synonym

@@ -171,6 +172,14 @@ namespace Microsoft.Dafny
           AllowGlobals = true;

           return true;

 

+        case "countVerificationErrors": {

+          int countErrors = 1; // defaults to reporting verification errors

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

+            CountVerificationErrors = countErrors == 1;

+          }

+          return true;

+        }

+

         default:

           break;

       }

@@ -245,7 +254,7 @@ 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 (*,/,%). 

+  /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.

@@ -256,6 +265,11 @@ namespace Microsoft.Dafny
                 a transition from the behavior in the language prior to version 1.9.3, from

                 which point onward all functions and methods declared at the module scope are

                 implicitly static and fields declarations are not allowed at the module scope.

+  /countVerificationErrors:<n>

+                0 - If preprocessing succeeds, set exit code to 0 regardless of the number

+                    of verification errors.

+                1 (default) - If preprocessing succeeds, set exit code to the number of

+                              verification errors.

 ");

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

     }