summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Michal Moskal <michal@moskal.me>2011-09-23 09:53:32 -0700
committerGravatar Michal Moskal <michal@moskal.me>2011-09-23 09:53:32 -0700
commit0a4cbcf2c32fe6f86df7e6d0ef159b04db6bbc5d (patch)
tree98db4885fca45a6152561fd68013a96e55384abd
parenta301c43eb80f9265de58709e1f47af2a86cc85da (diff)
Add handling of union active options
-rw-r--r--Source/ModelViewer/VccProvider.cs25
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)) {