Add handling of union active options

1 files changed, 22 insertions, 3 deletions

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index a11199f6..615dd8ff 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -38,7 +38,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
                                f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t, f_select_ptr,

                                f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state,

                                f_int_to_version, f_int_to_ptrset, f_set_in0, f_is_ghost_field, f_is_phys_field, f_idx, f_field_plus,

-                               f_is_sequential_field, f_is_volatile_field, f_type_project_0, f_array;

+                               f_is_sequential_field, f_is_volatile_field, f_type_project_0, f_array, f_active_option, f_int_to_field;

     public readonly Model.Element tp_object, tp_mathint, tp_bool, tp_state, tp_ptrset, tp_heaptp;

     public readonly Model.Element elt_me, elt_null;

     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();

@@ -69,6 +69,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_closed = m.MkFunc("$f_closed", 1);

       f_roots = m.MkFunc("$roots", 1);

       f_timestamps = m.MkFunc("$f_timestamp", 1);

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

       f_field = m.MkFunc("$field", 1);

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

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

@@ -79,6 +80,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_good_state = m.MkFunc("$good_state", 1);

       f_int_to_version = m.MkFunc("$int_to_version", 1);

       f_int_to_ptrset = m.MkFunc("$int_to_ptrset", 1);

+      f_int_to_field = m.MkFunc("$int_to_field", 1);

       f_set_in0 = m.MkFunc("$set_in0", 2);

       f_is_ghost_field = m.MkFunc("$is_ghost_field", 1);

       f_is_phys_field = m.MkFunc("$is_phys_field", 1);

@@ -518,7 +520,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return res;

     }

 

-    public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root" };

+    public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root", "$f_active_option" };

 

     public string ConstantFieldName(Model.Element elt)

     {

@@ -847,7 +849,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
                 continue;              

               var addr = f_ptr.TryEval(field, elt);

               if (addr != null) addresses.Add(addr);

-              BuildFieldNode(result, state, addr, field, val, addr);

+              var node = ComputeUnionActiveOption(state, elt, val, field);

+              if (node != null)

+                result.Add(node);

+              else

+                BuildFieldNode(result, state, addr, field, val, addr);

             }

           }

           //result.Sort(CompareFields);

@@ -974,6 +980,19 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       return result;

     }

 

+    private FieldNode ComputeUnionActiveOption(StateNode state, Model.Element elt, Model.Element val, Model.Element field)

+    {

+      if (f_active_option.AppsWithResult(field).FirstOrDefault() != null) {

+        var activeOpt = f_ptr.OptEval(f_int_to_field.OptEval(val), elt);

+        if (activeOpt != null) {

+          var nm = ConstantFieldName(field);

+          var fieldNode = new FieldNode(state, new EdgeName(nm), activeOpt, GuessType(activeOpt)) { Category = NodeCategory.MethodologyProperty };

+          return fieldNode;

+        }

+      }

+      return null;

+    }

+

     private void AddCasts(StateNode state, Model.Element elt, List<ElementNode> result)

     {

       foreach (var app in f_phys_ptr_cast.AppsWithArg(0, elt)) {