BVD: fixed two basic but damning problems with the Dafny provider, and elided some temporary variables

3 files changed, 8 insertions, 4 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 23b50a07..ab6e2435 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3988,7 +3988,7 @@ namespace Microsoft.Dafny {
         lhsTypes.Add(lhs.Type);

         if (bLhss[i] == null) {  // (in the current implementation, the second parameter "true" to ProcessLhss implies that all bLhss[*] will be null)

           // create temporary local and assign it to bLhss[i]

-          string nm = "$rhs#" + otherTmpVarCount;

+          string nm = "$rhs##" + otherTmpVarCount;

           otherTmpVarCount++;

           var ty = TrType(lhs.Type);

           Bpl.Expr wh = GetWhereClause(lhs.tok, new Bpl.IdentifierExpr(lhs.tok, nm, ty), lhs.Type, etran);

@@ -4055,7 +4055,7 @@ namespace Microsoft.Dafny {
       Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

       for (int i = 0; i < method.Ins.Count; i++) {

         Formal p = method.Ins[i];

-        VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost);

+        VarDecl local = new VarDecl(p.tok, p.Name + "#", p.Type, p.IsGhost);

         local.type = local.OptionalType;  // resolve local here

         IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);

         ie.Var = local; ie.Type = ie.Var.Type;  // resolve ie here

@@ -4093,7 +4093,7 @@ namespace Microsoft.Dafny {
         var bLhs = Lhss[i];

         if (ExpressionTranslator.ModeledAsBoxType(method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(LhsTypes[i])) {

           // we need an Unbox

-          Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp#" + otherTmpVarCount, predef.BoxType));

+          Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, "$tmp##" + otherTmpVarCount, predef.BoxType));

           otherTmpVarCount++;

           locals.Add(var);

           Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(bLhs.tok, var.Name, predef.BoxType);

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);