diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-26 16:52:40 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-26 16:52:40 -0700 |
| commit | 3d2bdaf737810142e8685296813562e7e29c9952 (patch) | |
| tree | f21e06c22006cc81bf2defc87e824019b3a79e19 /Source/ModelViewer | |
| parent | b9fba0c917f1a5489e92af4c0ef61130329ba123 (diff) | |
BVD: fixed two basic but damning problems with the Dafny provider, and elided some temporary variables
Diffstat (limited to 'Source/ModelViewer')
| -rw-r--r-- | Source/ModelViewer/DafnyProvider.cs | 4 | ||||
| -rw-r--r-- | Source/ModelViewer/Namer.cs | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs index 32912113..328bbb26 100644 --- a/Source/ModelViewer/DafnyProvider.cs +++ b/Source/ModelViewer/DafnyProvider.cs @@ -92,9 +92,13 @@ namespace Microsoft.Boogie.ModelViewer.Dafny {
if (name.StartsWith("$")) // this covers $Heap and $_Frame and $nw...
return null;
+ if (name.Contains("##")) // a temporary variable of the translation
+ return null;
+#if SOMETIME_AGAIN
var hash = name.IndexOf('#');
if (0 < hash)
return name.Substring(0, hash);
+#endif
return name;
}
diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs index fce9522d..1006c658 100644 --- a/Source/ModelViewer/Namer.cs +++ b/Source/ModelViewer/Namer.cs @@ -530,7 +530,7 @@ namespace Microsoft.Boogie.ModelViewer protected virtual string Format()
{
- if (args.Length == 0)
+ if (args == null || args.Length == 0)
return format;
var res = new StringBuilder(format.Length);
|