From 94e41cbfcdaa564c5027c66a8c25017eaabc964e Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Fri, 23 Sep 2011 16:01:34 -0700
Subject: BVD/VCC: Handle reading records/data types from memory

---
 Source/ModelViewer/VccProvider.cs | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index a9203e6b..165c8ac9 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -687,7 +687,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       Model.FuncTuple tpl;
       var kind = GetKind(tp, out tpl);
 
-      if (kind == DataKind.Flat) return elt;
+      if (kind == DataKind.Flat) {
+        if (elt.Kind == Model.ElementKind.Integer) {
+          var tpname = TypeName(tp);
+          if(tpname.StartsWith("$")) tpname = tpname.Substring(1);
+          foreach (var tupl in elt.References) {
+            if (tupl.Args.Length == 1 && tupl.Args[0] == elt && tupl.Func.Name.StartsWith("$int_to_") && tupl.Func.Name.EndsWith(tpname)) {
+              return tupl.Result;
+            }
+          }
+        }
+        return elt;
+      }
 
       if (kind == DataKind.Map) {
         if (elt.Kind == Model.ElementKind.Integer) {
-- 
cgit v1.2.3