diff options
author | qadeer <qadeer@microsoft.com> | 2011-08-09 16:14:02 -0700 |
---|---|---|
committer | qadeer <qadeer@microsoft.com> | 2011-08-09 16:14:02 -0700 |
commit | 0632aff3b94cae8d1856c77a12c1884cacda7c96 (patch) | |
tree | 75c3c74c2e71e1585a15158a9f648452244cb0c4 /Source/BoogieDriver | |
parent | 9a23bb4c570ca1c6cf401a89800b5181ad566ea5 (diff) |
further updates to bit vector analysis
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 3981536f..8262f749 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -155,6 +155,13 @@ namespace Microsoft.Boogie { return;
//BoogiePL.Errors.count = 0;
+ // Do bitvector analysis
+ if (CommandLineOptions.Clo.DoBitVectorAnalysis) {
+ Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);
+ PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false);
+ return;
+ }
+
oc = EliminateDeadVariablesAndInline(program);
//BoogiePL.Errors.count = 0;
@@ -360,11 +367,6 @@ namespace Microsoft.Boogie { // Eliminate dead variables
Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
- // Do bitvector analysis
- if (CommandLineOptions.Clo.DoBitVectorAnalysis) {
- Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);
- }
-
// Collect mod sets
if (CommandLineOptions.Clo.DoModSetAnalysis) {
Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
|