From d16580f98fe091ff59336b978df4705e2a63bcda Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Tue, 14 Dec 2010 23:31:04 +0000
Subject: Add information about field being volatile

---
 Source/Model/Model.cs             |  9 +++++++++
 Source/ModelViewer/VccProvider.cs | 28 +++++++++++++++++++++++-----
 2 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index c7314ca4..7201aa99 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -208,6 +208,15 @@ namespace Microsoft.Boogie
         return r != null && r.Value;
       }
 
+      /// <summary>
+      /// Short for TryEval(args) == (Element)false
+      /// </summary>
+      public bool IsFalse(params Element[] args)
+      {
+        var r = TryEval(args) as Boolean;
+        return r != null && !r.Value;
+      }
+
       public void AddApp(Element res, params Element[] args)
       {        
         if (Arity == 0)
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 6022819a..edff5abb 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -38,7 +38,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     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, 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_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;
     public readonly Model.Element tp_object, tp_mathint, tp_bool, tp_state, tp_ptrset;
     public readonly Model.Element elt_me, elt_null;
     Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
@@ -82,6 +83,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       f_is_phys_field = m.MkFunc("$is_phys_field", 1);
       f_idx = m.MkFunc("$idx", 2);
       f_field_plus = m.MkFunc("$field_plus", 2);
+      f_is_sequential_field = m.MkFunc("$is_sequential_field", 1);
+      f_is_volatile_field = m.MkFunc("$is_volatile_field", 1);
 
       tp_bool = m.GetFunc("^^bool").GetConstant();
       tp_mathint = m.GetFunc("^^mathint").GetConstant();
@@ -522,10 +525,25 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     void AddPtrType(StateNode state, Model.Element elt, List<ElementNode> res)
     {
       var f = f_field.TryEval(elt);
-      if (f != null)
-        f = f_field_type.TryEval(f);
-      if (f != null) {
-        res.Add(new FieldNode(state, new EdgeName("\\typeof"), f, tp_mathint) { Category = NodeCategory.MethodologyProperty });
+      if (f == null) return;
+
+      var tp = f_field_type.TryEval(f);
+      
+      var seq = "";
+
+      var is_seq = f_is_sequential_field.TryEval(f) as Model.Boolean;
+      var is_vol = f_is_volatile_field.TryEval(f) as Model.Boolean;
+
+      if (is_seq != null && is_vol != null && is_seq.Value == is_vol.Value) {
+        seq = " (volatile/sequential mismatch)";
+      } else if ((is_seq != null && is_seq.Value) || (is_vol != null && !is_vol.Value)) {
+          seq = " (sequential)";
+      } else if ((is_seq != null && !is_seq.Value) || (is_vol != null && is_vol.Value)) {
+          seq = " (volatile)";
+      }
+      
+      if (tp != null || seq != "") {
+        res.Add(new FieldNode(state, new EdgeName("\\typeof" + seq), tp, tp_mathint) { Category = NodeCategory.MethodologyProperty });
       }
     }
 
-- 
cgit v1.2.3