diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 16 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 3 |
2 files changed, 16 insertions, 3 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
}
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 854269c1..a769b829 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -104,9 +104,8 @@ namespace Microsoft.Dafny Console.WriteLine("Press Enter to exit.");
Console.ReadLine();
}
- if (CommandLineOptions.Clo.UseBaseNameForFileName && exitValue != ExitValue.PREPROCESSING_ERROR)
+ if (!DafnyOptions.O.CountVerificationErrors && exitValue != ExitValue.PREPROCESSING_ERROR)
{
- // TODO(wuestholz): We should probably add a separate flag for this. This is currently only used by the new testing infrastructure.
return 0;
}
//Console.ReadKey();
|