diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-09-23 16:01:34 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-09-23 16:01:34 -0700 |
| commit | 94e41cbfcdaa564c5027c66a8c25017eaabc964e (patch) | |
| tree | d007b62bd81a8bf2165ba4b3add72d4d06748fe8 /Source/ModelViewer | |
| parent | ad918ee2053574d3c2ea1b9299a59c392497457b (diff) | |
BVD/VCC: Handle reading records/data types from memory
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 13 |
1 files changed, 12 insertions, 1 deletions
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) {
|