blob: 0f713d9e0482a97799f3f82db87f95d86fe80980 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
namespace Microsoft.Boogie.ModelViewer.Vcc
{
public class Provider : ILanguageProvider
{
public static Provider Instance = new Provider();
private Provider() { }
public bool IsMyModel(Model m)
{
return m.TryGetFunc("$is_ghost_field") != null && m.TryGetFunc("$fk_vol_version") != null;
}
public IEnumerable<IDisplayNode> GetStates(Model m)
{
var vm = new VccModel();
foreach (var s in m.States) {
var sn = new StateNode(vm, s);
vm.states.Add(sn);
}
return vm.states;
}
}
class VccModel
{
public List<StateNode> states = new List<StateNode>();
public string GetUserVariableName(string name)
{
if (name.StartsWith("L#") || name.StartsWith("P#"))
return name.Substring(2);
return null;
}
}
class StateNode : DisplayNode
{
Model.CapturedState state;
VccModel parent;
List<VariableNode> vars = new List<VariableNode>();
public StateNode(VccModel parent, Model.CapturedState s) : base(s.Name)
{
this.parent = parent;
state = s;
var idx = name.LastIndexOfAny(new char[] { '\\', '/' });
if (idx > 0)
name = name.Substring(idx + 1);
var prev = parent.states.Last();
foreach (var v in state.Variables) {
var n = parent.GetUserVariableName(v);
if (n != null){
var vn = new VariableNode(n, state.TryGet(v));
vn.realName = n;
vars.Add(vn);
}
}
}
public override IEnumerable<string> Values
{
get { return vars.Map(v => v.Name); }
}
public override bool Expandable { get { return true; } }
public override IEnumerable<IDisplayNode> Expand()
{
foreach (var v in vars) yield return v;
}
}
public class VariableNode : DisplayNode
{
protected Model.Element elt;
public string realName;
public bool updatedHere;
public VariableNode(string name, Model.Element elt) : base(name)
{
this.elt = elt;
}
public override IEnumerable<string> Values
{
get
{
if (!(elt is Model.Uninterpreted))
yield return elt.ToString();
foreach (var tupl in elt.Names) {
if (tupl.Func.Arity == 0)
yield return tupl.Func.Name;
}
}
}
}
}
|
