From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/ModelViewer/BCTProvider.cs | 294 +++++++++++++++++++------------------- 1 file changed, 147 insertions(+), 147 deletions(-) (limited to 'Source/ModelViewer/BCTProvider.cs') diff --git a/Source/ModelViewer/BCTProvider.cs b/Source/ModelViewer/BCTProvider.cs index 6b48c396..3126084f 100644 --- a/Source/ModelViewer/BCTProvider.cs +++ b/Source/ModelViewer/BCTProvider.cs @@ -1,147 +1,147 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; - -namespace Microsoft.Boogie.ModelViewer.BCT { - public class Provider : ILanguageProvider { - public static Provider Instance = new Provider(); - private Provider() { } - - public bool IsMyModel(Model m) { - return m.TryGetFunc("$Alloc") != null; - } - - public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts) { - var dm = new BCTModel(m, opts); - foreach (var s in m.States) { - var sn = new StateNode(dm.states.Count, dm, s); - dm.states.Add(sn); - } - dm.FinishStates(); - return dm; - } - } - - class BCTModel : LanguageModel { - public readonly Model.Func f_heap_select; - public readonly Dictionary ArrayLengths = new Dictionary(); - Dictionary typeName = new Dictionary(); - public List states = new List(); - - public BCTModel(Model m, ViewOptions opts) - : base(m, opts) { - f_heap_select = m.MkFunc("[3]", 3); - - foreach (Model.Func fn in m.Functions) { - - } - } - - internal void FinishStates() { - GenerateSourceLocations(states); - } - - public override IEnumerable States { - get { return states; } - } - - public string GetUserVariableName(string name) { - if (name == "$this") - return "this"; - if (name.Contains("$")) - return null; - if (name == "isControlChecked" || name == "isControlEnabled") - return null; - return name; - } - - public Model.Element Image(Model.Element elt, Model.Func f) { - var r = f.AppWithResult(elt); - if (r != null) - return r.Args[0]; - return null; - } - - public IEnumerable GetExpansion(StateNode state, Model.Element elt) { - List result = new List(); - return result; - } - } - - class StateNode : NamedState { - internal readonly BCTModel dm; - internal readonly List vars = new List(); - internal readonly int index; - - public StateNode(int i, BCTModel parent, Model.CapturedState s) - : base(s, parent) { - dm = parent; - state = s; - index = i; - - SetupVars(); - } - - void SetupVars() { - var names = Util.Empty(); - - if (dm.states.Count > 0) { - var prev = dm.states.Last(); - names = prev.vars.Map(v => v.realName); - } - - names = names.Concat(state.Variables).Distinct(); - - var curVars = state.Variables.ToDictionary(x => x); - foreach (var v in names) { - if (dm.GetUserVariableName(v) != null) { - var val = state.TryGet(v); - var vn = new VariableNode(this, v, val); - vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v); - if (curVars.ContainsKey(v)) - dm.RegisterLocalValue(vn.Name, val); - vars.Add(vn); - } - } - - dm.Flush(Nodes); - } - - public override IEnumerable Nodes { - get { - return vars; - } - } - } - - class ElementNode : DisplayNode { - protected StateNode stateNode; - protected Model.Element elt; - protected BCTModel vm { get { return stateNode.dm; } } - - public ElementNode(StateNode st, EdgeName name, Model.Element elt) - : base(st.dm, name, elt) { - this.stateNode = st; - this.elt = elt; - } - - public ElementNode(StateNode st, string name, Model.Element elt) - : this(st, new EdgeName(name), elt) { } - - protected override void ComputeChildren() { - children.AddRange(vm.GetExpansion(stateNode, elt)); - } - } - - class VariableNode : ElementNode { - public bool updatedHere; - public string realName; - - public VariableNode(StateNode par, string realName, Model.Element elt) - : base(par, realName, elt) { - this.realName = realName; - name = new EdgeName(vm.GetUserVariableName(realName)); - } - } -} +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace Microsoft.Boogie.ModelViewer.BCT { + public class Provider : ILanguageProvider { + public static Provider Instance = new Provider(); + private Provider() { } + + public bool IsMyModel(Model m) { + return m.TryGetFunc("$Alloc") != null; + } + + public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts) { + var dm = new BCTModel(m, opts); + foreach (var s in m.States) { + var sn = new StateNode(dm.states.Count, dm, s); + dm.states.Add(sn); + } + dm.FinishStates(); + return dm; + } + } + + class BCTModel : LanguageModel { + public readonly Model.Func f_heap_select; + public readonly Dictionary ArrayLengths = new Dictionary(); + Dictionary typeName = new Dictionary(); + public List states = new List(); + + public BCTModel(Model m, ViewOptions opts) + : base(m, opts) { + f_heap_select = m.MkFunc("[3]", 3); + + foreach (Model.Func fn in m.Functions) { + + } + } + + internal void FinishStates() { + GenerateSourceLocations(states); + } + + public override IEnumerable States { + get { return states; } + } + + public string GetUserVariableName(string name) { + if (name == "$this") + return "this"; + if (name.Contains("$")) + return null; + if (name == "isControlChecked" || name == "isControlEnabled") + return null; + return name; + } + + public Model.Element Image(Model.Element elt, Model.Func f) { + var r = f.AppWithResult(elt); + if (r != null) + return r.Args[0]; + return null; + } + + public IEnumerable GetExpansion(StateNode state, Model.Element elt) { + List result = new List(); + return result; + } + } + + class StateNode : NamedState { + internal readonly BCTModel dm; + internal readonly List vars = new List(); + internal readonly int index; + + public StateNode(int i, BCTModel parent, Model.CapturedState s) + : base(s, parent) { + dm = parent; + state = s; + index = i; + + SetupVars(); + } + + void SetupVars() { + var names = Util.Empty(); + + if (dm.states.Count > 0) { + var prev = dm.states.Last(); + names = prev.vars.Map(v => v.realName); + } + + names = names.Concat(state.Variables).Distinct(); + + var curVars = state.Variables.ToDictionary(x => x); + foreach (var v in names) { + if (dm.GetUserVariableName(v) != null) { + var val = state.TryGet(v); + var vn = new VariableNode(this, v, val); + vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v); + if (curVars.ContainsKey(v)) + dm.RegisterLocalValue(vn.Name, val); + vars.Add(vn); + } + } + + dm.Flush(Nodes); + } + + public override IEnumerable Nodes { + get { + return vars; + } + } + } + + class ElementNode : DisplayNode { + protected StateNode stateNode; + protected Model.Element elt; + protected BCTModel vm { get { return stateNode.dm; } } + + public ElementNode(StateNode st, EdgeName name, Model.Element elt) + : base(st.dm, name, elt) { + this.stateNode = st; + this.elt = elt; + } + + public ElementNode(StateNode st, string name, Model.Element elt) + : this(st, new EdgeName(name), elt) { } + + protected override void ComputeChildren() { + children.AddRange(vm.GetExpansion(stateNode, elt)); + } + } + + class VariableNode : ElementNode { + public bool updatedHere; + public string realName; + + public VariableNode(StateNode par, string realName, Model.Element elt) + : base(par, realName, elt) { + this.realName = realName; + name = new EdgeName(vm.GetUserVariableName(realName)); + } + } +} -- cgit v1.2.3