diff options
| author |  Michal Moskal <michal@moskal.me> | 2012-01-28 17:20:46 -0500 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2012-01-28 17:20:46 -0500 |
| commit | 4afef98f9a86e41be450520cc4329e5e55e6c52b (patch) | |
| tree | 3864718fe23fbb0e745deaf1d48cbe1e1841c8d5 /Source/ModelViewer | |
| parent | 47919504d8535265a82de344795d93c78c9e8d83 (diff) | |
VCC: fixes in function visibility
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 574e6282..ea213aef 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -1038,7 +1038,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var edgname = new EdgeName(this, "[%0]", sel.Args[1]);
result.Add(new MapletNode(state, edgname, sel.Result, tp_bool) { Category = NodeCategory.Maplet });
}
- } else if (kind == DataKind.Flat && elt != null) {
+ } else if (kind == DataKind.Flat) {
foreach (var tupl in elt.References) {
if (tupl.Args.Length == 1 && tupl.Args[0] == elt) {
var fname = tupl.Func.Name;
@@ -1071,7 +1071,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var args = tupl.Args;
for (int i = 0; i < args.Length; ++i) {
if (args[i] == elt) seenSelf = true;
- else if (IsThisState(curState, args[i])) seenThisState = true;
+ if (IsThisState(curState, args[i])) seenThisState = true;
else if (IsSomeState(args[i])) seenState = true;
}
if (!seenSelf) continue; // not looking for aliases (maybe we should?)
|