diff options
Diffstat (limited to 'Source/Dafny/DafnyOptions.cs')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 170 |
1 files changed, 162 insertions, 8 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 4fc2de96..9258503b 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -9,18 +9,26 @@ namespace Microsoft.Dafny {
public class DafnyOptions : Bpl.CommandLineOptions
{
- public DafnyOptions()
+ private ErrorReporter errorReporter;
+
+ public DafnyOptions(ErrorReporter errorReporter = null)
: base("Dafny", "Dafny program verifier") {
+ this.errorReporter = errorReporter;
+ SetZ3ExecutableName();
}
public override string VersionNumber {
get {
- return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion;
+ return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion
+#if ENABLE_IRONDAFNY
+ + "[IronDafny]"
+#endif
+ ;
}
}
public override string VersionSuffix {
get {
- return " version " + VersionNumber + ", Copyright (c) 2003-2015, Microsoft.";
+ return " version " + VersionNumber + ", Copyright (c) 2003-2016, Microsoft.";
}
}
@@ -35,6 +43,7 @@ namespace Microsoft.Dafny Bpl.CommandLineOptions.Install(options);
}
+ public bool UnicodeOutput = false;
public bool DisallowSoundnessCheating = false;
public bool Dafnycc = false;
public int Induction = 3;
@@ -42,9 +51,10 @@ namespace Microsoft.Dafny public string DafnyPrelude = null;
public string DafnyPrintFile = null;
public enum PrintModes { Everything, NoIncludes, NoGhost };
- public PrintModes PrintMode;
+ public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
public bool DafnyVerify = true;
public string DafnyPrintResolvedFile = null;
+ public List<string> DafnyPrintExportedViews = new List<string>();
public bool Compile = true;
public bool ForceCompile = false;
public bool RunAfterCompile = false;
@@ -54,6 +64,21 @@ namespace Microsoft.Dafny public string AutoReqPrintFile = null;
public bool ignoreAutoReq = false;
public bool AllowGlobals = false;
+ public bool CountVerificationErrors = true;
+ public bool Optimize = false;
+ public bool AutoTriggers = true;
+ public bool RewriteFocalPredicates = true;
+ public bool PrintTooltips = false;
+ public bool PrintStats = false;
+ public bool PrintFunctionCallGraph = false;
+ public bool WarnShadowing = false;
+ public bool IronDafny =
+#if ENABLE_IRONDAFNY
+ true
+#else
+ false
+#endif
+ ;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -96,6 +121,11 @@ namespace Microsoft.Dafny DafnyPrintResolvedFile = args[ps.i];
}
return true;
+ case "view":
+ if (ps.ConfirmArgumentCount(1)) {
+ DafnyPrintExportedViews = args[ps.i].Split(',').ToList();
+ }
+ return true;
case "compile": {
int compile = 0;
@@ -154,7 +184,7 @@ namespace Microsoft.Dafny case "noNLarith":
DisableNLarith = true;
- this.AddZ3Option("NL_ARITH=false");
+ this.AddZ3Option("smt.arith.nl=false");
return true;
case "autoReqPrint":
@@ -170,6 +200,61 @@ namespace Microsoft.Dafny case "allowGlobals":
AllowGlobals = true;
return true;
+
+ case "stats":
+ PrintStats = true;
+ return true;
+
+ case "funcCallGraph":
+ PrintFunctionCallGraph = true;
+ return true;
+
+ case "warnShadowing":
+ WarnShadowing = true;
+ return true;
+
+ case "countVerificationErrors": {
+ int countErrors = 1; // defaults to reporting verification errors
+ if (ps.GetNumericArgument(ref countErrors, 2)) {
+ CountVerificationErrors = countErrors == 1;
+ }
+ return true;
+ }
+
+ case "printTooltips":
+ PrintTooltips = true;
+ return true;
+
+ case "autoTriggers": {
+ int autoTriggers = 0;
+ if (ps.GetNumericArgument(ref autoTriggers, 2)) {
+ AutoTriggers = autoTriggers == 1;
+ }
+ return true;
+ }
+
+ case "rewriteFocalPredicates": {
+ int rewriteFocalPredicates = 0;
+ if (ps.GetNumericArgument(ref rewriteFocalPredicates, 2)) {
+ RewriteFocalPredicates = rewriteFocalPredicates == 1;
+ }
+ return true;
+ }
+
+ case "optimize": {
+ Optimize = true;
+ return true;
+ }
+
+ case "noIronDafny": {
+ IronDafny = false;
+ return true;
+ }
+
+ case "ironDafny": {
+ IronDafny = true;
+ return true;
+ }
default:
break;
@@ -190,6 +275,39 @@ namespace Microsoft.Dafny // TODO: provide attribute help here
}
+
+ /// <summary>
+ /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency.
+ /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script.
+ /// For developers though (and people getting this from source), it's convenient to be able to run right away,
+ /// so we vendor a Windows version.
+ /// </summary>
+ private void SetZ3ExecutableName() {
+ var platform = (int)System.Environment.OSVersion.Platform;
+
+ // http://www.mono-project.com/docs/faq/technical/
+ var isUnix = platform == 4 || platform == 128;
+
+ var z3binName = isUnix ? "z3" : "z3.exe";
+ var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
+ var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin");
+ var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName);
+
+ if (!System.IO.File.Exists(z3BinPath) && !isUnix) {
+ // This is most likely a Windows user running from source without downloading z3
+ // separately; this is ok, since we vendor z3.exe.
+ z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName);
+ }
+
+ if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) {
+ var tok = new Bpl.Token(1, 1) { filename = "*** " };
+ errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.",
+ z3binName, z3BinDir, System.Environment.NewLine);
+ } else {
+ Z3ExecutablePath = z3BinPath;
+ }
+ }
+
public override void Usage() {
Console.WriteLine(@" ---- Dafny options ---------------------------------------------------------
@@ -202,6 +320,7 @@ namespace Microsoft.Dafny print Dafny program after parsing it
(use - as <file> to print to console)
/printMode:<Everything|NoIncludes|NoGhost>
+ Everything is the default.
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
@@ -209,6 +328,11 @@ namespace Microsoft.Dafny /rprint:<file>
print Dafny program after resolving it
(use - as <file> to print to console)
+ /view:<view1, view2>
+ print the filtered views of a module after it is resolved (/rprint).
+ if print before the module is resolved (/dprint), then everthing in the module is printed
+ if no view is specified, then everything in the module is printed.
+
/dafnyVerify:<n>
0 - stop after typechecking
1 - continue on to translation, verification, and compilation
@@ -237,7 +361,7 @@ namespace Microsoft.Dafny 2 - apply induction as requested (by attributes) and also
for heuristically chosen quantifiers
3 (default) - apply induction as requested, and for
- heuristically chosen quantifiers and ghost methods
+ heuristically chosen quantifiers and lemmas
/inductionHeuristic:<n>
0 - least discriminating induction heuristic (that is, lean
toward applying induction more often)
@@ -245,17 +369,47 @@ 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.
/noAutoReq Ignore autoReq attributes
/allowGlobals Allow the implicit class '_default' to contain fields, instance functions,
and instance methods. These class members are declared at the module scope,
- outside of explicit classes. This command-line option is provided to simply
+ outside of explicit classes. This command-line option is provided to simplify
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.
+ /autoTriggers:<n>
+ 0 - Do not generate {:trigger} annotations for user-level quantifiers.
+ 1 (default) - Add a {:trigger} to each user-level quantifier. Existing
+ annotations are preserved.
+ /rewriteFocalPredicates:<n>
+ 0 - Don't rewrite predicates in the body of prefix lemmas.
+ 1 (default) - In the body of prefix lemmas, rewrite any use of a focal predicate
+ P to P#[_k-1].
+ /optimize Produce optimized C# code, meaning:
+ - selects optimized C# prelude by passing
+ /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires
+ System.Collections.Immutable.dll in the source directory to successfully
+ compile).
+ - passes /optimize flag to csc.exe.
+ /stats Print interesting statistics about the Dafny files supplied.
+ /funcCallGraph Print out the function call graph. Format is: func,mod=callee*
+ /warnShadowing Emits a warning if the name of a declared variable caused another variable
+ to be shadowed
+ /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of
+ these features may cause your code to become incompatible with future
+ releases of Dafny.
+ /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default.
+ /printTooltips
+ Dump additional positional information (displayed as mouse-over tooltips by
+ the VS plugin) to stdout as 'Info' messages.
");
base.Usage(); // also print the Boogie options
}
|