From 0a4cbcf2c32fe6f86df7e6d0ef159b04db6bbc5d Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Fri, 23 Sep 2011 09:53:32 -0700
Subject: Add handling of union active options

---
 Source/ModelViewer/VccProvider.cs | 25 ++++++++++++++++++++++---
 1 file 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)) {
-- 
cgit v1.2.3