From 5f5f709c8f3924ddbfbb48f52b7875eac143503a Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Mon, 27 Oct 2014 13:26:43 -0700 Subject: Add an option to allow automatically generated requirements to be printed to a file, making them easier to inspect and manipulate. --- Source/Dafny/DafnyOptions.cs | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'Source/Dafny/DafnyOptions.cs') 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: + Print out requirements that were automatically generated by autoReq. "); base.Usage(); // also print the Boogie options } -- cgit v1.2.3