various changes to boogie for bitvector analysis and bctprovider

4 files changed, 16 insertions, 2 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 82c864d5..3981536f 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -360,6 +360,11 @@ 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);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index e1136150..c4c56f28 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -250,6 +250,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 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

 

@@ -1404,7 +1405,8 @@ 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("doModSetAnalysis", ref DoModSetAnalysis) ||

+              ps.CheckBooleanFlag("doBitVectorAnalysis", ref DoBitVectorAnalysis)

               ) {

               // one of the boolean flags matched

             } else if (ps.s.StartsWith("-") || ps.s.StartsWith("/")) {

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index c3ef425f..cff4f7f2 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -151,6 +151,7 @@
     <Compile Include="AbsyExpr.cs" />

     <Compile Include="AbsyQuant.cs" />

     <Compile Include="AbsyType.cs" />

+    <Compile Include="BitvectorAnalysis.cs" />

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="DeadVarElim.cs" />

     <Compile Include="Duplicator.cs" />

diff --git a/Source/ModelViewer/BCTProvider.cs b/Source/ModelViewer/BCTProvider.cs
index f7dae29e..6b48c396 100644
--- a/Source/ModelViewer/BCTProvider.cs
+++ b/Source/ModelViewer/BCTProvider.cs
@@ -32,6 +32,10 @@ namespace Microsoft.Boogie.ModelViewer.BCT {
     public BCTModel(Model m, ViewOptions opts)

       : base(m, opts) {

       f_heap_select = m.MkFunc("[3]", 3);

+

+      foreach (Model.Func fn in m.Functions) {

+

+      }

     }

 

     internal void FinishStates() {

@@ -43,7 +47,9 @@ namespace Microsoft.Boogie.ModelViewer.BCT {
     }

 

     public string GetUserVariableName(string name) {

-      if (name.StartsWith("$")) 

+      if (name == "$this")

+        return "this";

+      if (name.Contains("$")) 

         return null;

       if (name == "isControlChecked" || name == "isControlEnabled")

         return null;