further updates to bit vector analysis

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);