summaryrefslogtreecommitdiff
path: root/Source/Dafny/DafnyOptions.cs
diff options
context:
space:
mode:
authorGravatar Bryan Parno <parno@microsoft.com>2013-12-13 13:54:40 -0800
committerGravatar Bryan Parno <parno@microsoft.com>2013-12-13 13:54:40 -0800
commitbec9ceeba29e8513a41a65be5a8fdba8d68333e3 (patch)
tree667f7cd13eda61568c598d34e986605b6d10ade9 /Source/Dafny/DafnyOptions.cs
parent87cbe4be0506bd30df76a5640135fe8ccff08cc1 (diff)
Add a command-line option to disable include directives.
Diffstat (limited to 'Source/Dafny/DafnyOptions.cs')
-rw-r--r--Source/Dafny/DafnyOptions.cs6
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 9176b8e1..753fbb32 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -39,6 +39,7 @@ namespace Microsoft.Dafny
public bool Compile = true;
public bool ForceCompile = false;
public bool SpillTargetCode = false;
+ public bool DisallowIncludes = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -96,6 +97,10 @@ namespace Microsoft.Dafny
ps.GetNumericArgument(ref InductionHeuristic, 7);
return true;
+ case "noInclude":
+ DisallowIncludes = true;
+ return true;
+
default:
break;
}
@@ -154,6 +159,7 @@ namespace Microsoft.Dafny
1,2,3,4,5 - levels in between, ordered as follows as far as
how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6
6 (default) - most discriminating
+ /noIncludes Ignore include directives
");
base.Usage(); // also print the Boogie options
}