Make the tree actually work

3 files changed, 33 insertions, 14 deletions

diff --git a/Source/ModelViewer/Main.Designer.cs b/Source/ModelViewer/Main.Designer.cs
index 64164f0e..312a2766 100644
--- a/Source/ModelViewer/Main.Designer.cs
+++ b/Source/ModelViewer/Main.Designer.cs
@@ -54,7 +54,7 @@
       this.currentStateView.Name = "currentStateView";

       this.currentStateView.OwnerDraw = true;

       this.currentStateView.ShowItemToolTips = true;

-      this.currentStateView.Size = new System.Drawing.Size(654, 706);

+      this.currentStateView.Size = new System.Drawing.Size(614, 706);

       this.currentStateView.TabIndex = 0;

       this.currentStateView.UseCompatibleStateImageBehavior = false;

       this.currentStateView.View = System.Windows.Forms.View.Details;

@@ -74,7 +74,7 @@
       // value

       // 

       this.value.Text = "Value";

-      this.value.Width = 463;

+      this.value.Width = 394;

       // 

       // splitContainer1

       // 

@@ -90,7 +90,7 @@
       // 

       this.splitContainer1.Panel2.Controls.Add(this.stateList);

       this.splitContainer1.Size = new System.Drawing.Size(875, 706);

-      this.splitContainer1.SplitterDistance = 654;

+      this.splitContainer1.SplitterDistance = 614;

       this.splitContainer1.TabIndex = 1;

       // 

       // stateList

@@ -106,7 +106,7 @@
       this.stateList.MultiSelect = false;

       this.stateList.Name = "stateList";

       this.stateList.ShowItemToolTips = true;

-      this.stateList.Size = new System.Drawing.Size(217, 706);

+      this.stateList.Size = new System.Drawing.Size(257, 706);

       this.stateList.TabIndex = 0;

       this.stateList.UseCompatibleStateImageBehavior = false;

       this.stateList.View = System.Windows.Forms.View.Details;

@@ -115,7 +115,7 @@
       // columnHeader1

       // 

       this.columnHeader1.Text = "State";

-      this.columnHeader1.Width = 82;

+      this.columnHeader1.Width = 112;

       // 

       // columnHeader2

       // 

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 7aa992b6..2a53f72e 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -88,7 +88,7 @@ namespace Microsoft.Boogie.ModelViewer
 

     }

 

-    const int levelMult = 10;

+    const int levelMult = 16;

     const int plusWidth = 16;

 

     static StringFormat center = new StringFormat() { Alignment = StringAlignment.Center };

@@ -246,10 +246,12 @@ namespace Microsoft.Boogie.ModelViewer
     {

       get

       {

-        foreach (var c in children) {

-          yield return c;

-          foreach (var ch in c.RecChildren)

-            yield return ch;

+        if (expanded) {

+          foreach (var c in children) {

+            yield return c;

+            foreach (var ch in c.RecChildren)

+              yield return ch;

+          }

         }

       }

     }

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 97f22940..32557b0e 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -29,7 +29,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
   class VccModel

   {

     public readonly Model model;

-    public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field, f_select_value, f_field_type;

+    public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field, f_select_value, f_field_type, f_int_to_ptr, f_ptr_to_int;

 

     public VccModel(Model m)

     {

@@ -44,6 +44,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_select_field = m.MkFunc("Select_[$field][$ptr]$int", 2);

       f_select_value = m.MkFunc("Select_[$ptr]$int", 2);

       f_field_type = m.MkFunc("$field_type", 1);

+      f_int_to_ptr = m.MkFunc("$int_to_ptr", 1);

+      f_ptr_to_int = m.MkFunc("$ptr_to_int", 1);

     }

 

     public List<StateNode> states = new List<StateNode>();

@@ -89,16 +91,21 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       var deref = Image(tp, f_ptr_to);

       Model.Element casted = null;

 

+      var ptrElt = elt;

+      if (ptrElt.Kind == Model.ElementKind.Integer) {

+        ptrElt = f_int_to_ptr.TryEval(ptrElt);        

+      }

+

       if (deref != null) {

-        casted = f_phys_ptr_cast.TryEval(elt, deref);

+        casted = f_phys_ptr_cast.TryEval(ptrElt, deref);

       } else {

         deref = Image(tp, f_spec_ptr_to);

         if (deref != null)

-          casted = f_spec_ptr_cast.TryEval(elt, deref);

+          casted = f_spec_ptr_cast.TryEval(ptrElt, deref);

       }

 

       if (deref != null && casted == null)

-        casted = elt;

+        casted = ptrElt;

 

       if (casted != null) {

         var heap = state.state.TryGet("$s");

@@ -132,6 +139,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       var idx = name.LastIndexOfAny(new char[] { '\\', '/' });

       if (idx > 0)

         name = name.Substring(idx + 1);

+      var limit = 16;

+      if (name.Length > limit) {

+        idx = name.IndexOf('(');

+        if (idx > 0) {

+          var prefLen = limit - (name.Length - idx);

+          if (prefLen > 2) {

+            name = name.Substring(0,prefLen) + ".." + name.Substring(idx);

+          }

+        }

+      }

 

       var names = Util.Empty<string>();