diff options
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index c4c56f28..edca934c 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -251,6 +251,7 @@ namespace Microsoft.Boogie { public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
public bool DoModSetAnalysis = false;
public bool DoBitVectorAnalysis = false;
+ public string BitVectorAnalysisOutputBplFile = null;
public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation
public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
@@ -1364,6 +1365,14 @@ namespace Microsoft.Boogie { }
break;
+ case "-doBitVectorAnalysis":
+ case "/doBitVectorAnalysis":
+ DoBitVectorAnalysis = true;
+ if (ps.ConfirmArgumentCount(1)) {
+ BitVectorAnalysisOutputBplFile = args[ps.i];
+ }
+ break;
+
default:
Contract.Assume(true);
bool option = false;
@@ -1405,8 +1414,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
- ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
- ps.CheckBooleanFlag("doBitVectorAnalysis", ref DoBitVectorAnalysis)
+ ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis)
) {
// one of the boolean flags matched
} else if (ps.s.StartsWith("-") || ps.s.StartsWith("/")) {
|