Introduce states more aggressively. Show is_null() for pointers.

2 files changed, 23 insertions, 3 deletions

diff --git a/Source/ModelViewer/DataModel.cs b/Source/ModelViewer/DataModel.cs
index ff33231f..4a1acb42 100644
--- a/Source/ModelViewer/DataModel.cs
+++ b/Source/ModelViewer/DataModel.cs
@@ -246,6 +246,11 @@ namespace Microsoft.Boogie.ModelViewer
       foreach (var s in inp) fn(s);

     }

 

+    public static void AddRange<T>(this HashSet<T> st, IEnumerable<T> elts)

+    {

+      foreach (var e in elts) st.Add(e);

+    }

+

     public static T OrElse<T>(T a, T b)

       where T : class

     {

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index d86b6bcc..1fe322b4 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -128,16 +128,24 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       var i = 0;

       while (i < allStates.Length) {

         var lastGoodName = allStates[i].State.Name;

+        

+        var userVars = new HashSet<string>(allStates[i].State.Variables.Where(localVariableNames.ContainsKey));

         i++;

         while (i < allStates.Length) {          

-          if (allStates[i].State.Variables.Contains("$s"))

-            break;          

+          foreach (var v in allStates[i].State.Variables) {

+            if (v == "$s" || userVars.Contains(v)) goto stop;

+            if (localVariableNames.ContainsKey(v))

+              userVars.Add(v);

+          }

+

           var curName = TryParseSourceLocation(allStates[i].State.Name);

           if (!IsBadName(curName))

             lastGoodName = allStates[i].State.Name;

           i++;

         }

 

+      stop: 

+

         var lastState = allStates[i - 1];

         lastState.capturedStateName = lastGoodName;

         lastState.index = states.Count;

@@ -1025,6 +1033,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       if (name != "")

         return name;

 

+      var isNull = false;

       foreach (var tpl in elt.References) {

         var fn = tpl.Func;

         if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)

@@ -1040,6 +1049,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         if (tpl.Result == elt)

           if (fn == f_int_to_version)

             return "version";

+

+        if (fn == f_is_null && tpl.Result == model.True) 

+          isNull = true;

       }

 

       var fld = vm.f_field.TryEval(elt);

@@ -1047,8 +1059,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         var tp = vm.f_field_type.TryEval(fld);

         if (tp != null) {

           var n = vm.TryTypeName(tp);

-          if (n != null)

+          if (n != null) {

+            if (isNull)

+              return "(" + n + "*)NULL";

             return n;

+          }

         }

       }