diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-10-19 11:57:14 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-10-19 11:57:14 -0700 |
| commit | 2324cef1837e957bfe85c03aea84e3ea2aab22ad (patch) | |
| tree | b1b00183016a67aa35a7ee1ed0ac5599ebfde048 /Source/ModelViewer/VccProvider.cs | |
| parent | f33e5329fc935e1d3ef3c1ef53bb4c09c96b1e23 (diff) | |
VCC: Fix problem with booleans being displayed as maps
Diffstat (limited to 'Source/ModelViewer/VccProvider.cs')
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 78b280ee..8d2ece08 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -558,7 +558,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc }
if (name.Contains('#')) score -= 1;
} else if (synthethic_fields.Contains(t.Func.Name)) {
- name = string.Format("{0}<{1}>", t.Func.Name.Substring(3), TypeName(t.Args[0]));
+ name = string.Format("{0}<{1}>", t.Func.Name.Substring(3).Replace("root", "alloc_root"), TypeName(t.Args[0]));
score = 5;
}
if (score > bestScore) {
@@ -696,9 +696,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc 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;
+ if (tpname.StartsWith("#")) {
+ 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;
+ }
}
}
}
|