diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 1 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 2 | ||||
| -rw-r--r-- | Source/ModelViewer/VccProvider.cs | 92 |
3 files changed, 79 insertions, 16 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index d2bdee62..a3bb44ba 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -264,7 +264,6 @@ namespace Microsoft.Boogie { /// <param name="args">Consumed ("captured" and possibly modified) by the method.</param>
public bool Parse([Captured] string[]/*!*/ args) {
Contract.Requires(cce.NonNullElements(args));
- Contract.Ensures(-2 <= Contract.Result<int>() && Contract.Result<int>() <= 2 && Contract.Result<int>() != 0);
// save the command line options for the log files
Environment += "Command Line Options: " + args.Concat(" ");
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 1d55fc13..e4dd3e46 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -444,7 +444,7 @@ namespace Microsoft.Boogie.ModelViewer private void ExpandParents(SkeletonItem item)
{
item = item.parent;
- while (item != null && !item.Expanded) {
+ while (item != null) {
item.Expanded = true;
item = item.parent;
}
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 10e4db10..6fd068a8 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -48,9 +48,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc public List<StateNode> states = new List<StateNode>();
public Dictionary<string, string> localVariableNames = new Dictionary<string, string>();
+ Dictionary<Model.Element, string> datatypeLongName = new Dictionary<Model.Element, string>();
+
Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();
public const string selfMarker = "\\self";
+ public const int maxDatatypeNameLength = 5;
public VccModel(Model m, ViewOptions opts)
: base(m, opts)
@@ -422,6 +425,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc return name.Substring(5);
}
+ if (name == "$result") {
+ kind = "function return value";
+ return "\\result";
+ }
+
if (name.StartsWith("res__") && viewOpts.ViewLevel >= 1) {
kind = "call result";
return name;
@@ -686,7 +694,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var fldName = tpl.Func.Name.Substring(3);
var idx = fldName.LastIndexOf('.');
if (idx > 0) {
- return fldName.Substring(0, idx).Replace("_vcc_math_type_", ""); + return fldName.Substring(0, idx).Replace("_vcc_math_type_", "");
}
}
@@ -1197,7 +1205,58 @@ namespace Microsoft.Boogie.ModelViewer.Vcc }
}
- private string CanonicalBaseNameCore(string name, Model.Element elt)
+ private int DataTypeToString(StringBuilder sb, int level, Model.Element elt)
+ {
+ Model.FuncTuple ctor = null;
+ int len = 1;
+ string dataTypeType = null;
+ foreach (var app in elt.References) {
+ var n = app.Func.Name;
+ if (app.Result == elt && n.StartsWith("DF#")) {
+ ctor = app;
+ }
+ var tmp = DataTypeName(elt, app);
+ if (tmp != null) dataTypeType = tmp;
+ }
+
+ if (dataTypeType != null) {
+ if (ctor != null)
+ sb.Append(ctor.Func.Name.Substring(3));
+ else
+ sb.Append(DataTypeShortName(elt, dataTypeType));
+ if (ctor != null && ctor.Args.Length > 0) {
+ if (level <= 0) sb.Append("(...)");
+ else {
+ sb.Append("(");
+ for (int i = 0; i < ctor.Args.Length; ++i) {
+ if (i != 0) sb.Append(", ");
+ len += DataTypeToString(sb, level - 1, ctor.Args[i]);
+ }
+ sb.Append(")");
+ }
+ }
+ } else {
+ sb.Append(CanonicalName(elt));
+ }
+ return len;
+ }
+
+ private string DataTypeShortName(Model.Element elt, string tp)
+ {
+ var baseName = tp;
+
+ var hd = model.MkFunc("DGH#" + tp, 1).TryEval(elt);
+ if (hd != null) {
+ foreach (var nm in hd.References) {
+ if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
+ baseName = nm.Func.Name.Substring(3);
+ }
+ }
+
+ return baseName;
+ }
+
+ private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff)
{
var vm = this;
@@ -1229,18 +1288,19 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var dtpName = DataTypeName(elt, tpl);
if (dtpName != null) {
- var dgh = model.TryGetFunc("DGH#" + dtpName);
- if (dgh != null) {
- var hd = dgh.TryEval(elt);
- if (hd != null) {
- foreach (var nm in hd.References) {
- if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
- return nm.Func.Name.Substring(3);
- }
-
- }
+ var sb = new StringBuilder();
+ string prev = null;
+ datatypeLongName[elt] = "*SELF*"; // in case we recurse (but this shouldn't happen)
+ for (int lev = 0; lev < 10; lev++) {
+ sb.Length = 0;
+ var len = DataTypeToString(sb, lev, elt);
+ if (prev == null || len <= maxDatatypeNameLength)
+ prev = sb.ToString();
}
- return dtpName;
+
+ datatypeLongName[elt] = prev;
+ suff = NameSeqSuffix.WhenNonZero;
+ return prev;
}
}
@@ -1267,9 +1327,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc suff = NameSeqSuffix.None;
return lit;
}
+ if (datatypeLongName.TryGetValue(elt, out lit)) {
+ suff = NameSeqSuffix.WhenNonZero;
+ return lit;
+ }
var name = base.CanonicalBaseName(elt, out suff);
- name = CanonicalBaseNameCore(name, elt);
+ name = CanonicalBaseNameCore(name, elt, true, ref suff);
return name;
}
|