summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-08-08 13:03:37 -0700
committerGravatar qadeer <qadeer@microsoft.com>2011-08-08 13:03:37 -0700
commitb56539ef83628c27e0d32b0ef595263f40836c44 (patch)
tree456031e52cfeddf442691bfc62f14232eede5617 /Source
parent87946bf9c24a394c93dc3ffbae7c544640e8c120 (diff)
various changes to boogie for bitvector analysis and bctprovider
Diffstat (limited to 'Source')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs5
-rw-r--r--Source/Core/CommandLineOptions.cs4
-rw-r--r--Source/Core/Core.csproj1
-rw-r--r--Source/ModelViewer/BCTProvider.cs8
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;