Fix issue 113. Make sure the tempVar name used in ToString() method doesn't

collide with the names of its formals.

3 files changed, 42 insertions, 6 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 69b7a32d..264ecf9b 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -473,22 +473,23 @@ namespace Microsoft.Dafny {
           } else {

             nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;

           }

-          Indent(ind + IndentAmount, wr); wr.WriteLine("string s = \"{0}\";", nm);

+          var tempVar = GenVarName("s", ctor.Formals);

+          Indent(ind + IndentAmount, wr); wr.WriteLine("string {0} = \"{1}\";", tempVar, nm);

           if (ctor.Formals.Count != 0) {

-            Indent(ind + IndentAmount, wr); wr.WriteLine("s += \"(\";");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += \"(\";", tempVar);

             i = 0;

             foreach (var arg in ctor.Formals) {

               if (!arg.IsGhost) {

                 if (i != 0) {

-                  Indent(ind + IndentAmount, wr); wr.WriteLine("s += \", \";");

+                  Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += \", \";", tempVar);

                 }

-                Indent(ind + IndentAmount, wr); wr.WriteLine("s += @{0}.ToString();", FormalName(arg, i));

+                Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += @{1}.ToString();", tempVar,FormalName(arg, i));

                 i++;

               }

             }

-            Indent(ind + IndentAmount, wr); wr.WriteLine("s += \")\";");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("{0} += \")\";", tempVar);

           }

-          Indent(ind + IndentAmount, wr); wr.WriteLine("return s;");

+          Indent(ind + IndentAmount, wr); wr.WriteLine("return {0};", tempVar);

           Indent(ind, wr); wr.WriteLine("}");

         }

 

@@ -497,6 +498,25 @@ namespace Microsoft.Dafny {
       constructorIndex++;

     }

 

+    // create a varName that is not a duplicate of formals' name

+    string GenVarName(string root, List<Formal> formals) {

+      bool finished = false;

+      while (!finished) {

+        finished = true;

+        int i = 0;

+        foreach (var arg in formals) {

+          if (!arg.IsGhost) {

+            if (root.Equals(FormalName(arg, i))) {

+              root += root;

+              finished = false;

+            }

+            i++;

+          }

+        }

+      }

+      return root;

+    }

+

     void CompileDatatypeStruct(DatatypeDecl dt, int indent, TextWriter wr) {

       Contract.Requires(dt != null);

 

diff --git a/Test/dafny4/Bug113.dfy b/Test/dafny4/Bug113.dfy
new file mode 100644
index 00000000..8f5ddf9f
--- /dev/null
+++ b/Test/dafny4/Bug113.dfy
@@ -0,0 +1,10 @@
+// RUN: %dafny /compile:3  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+datatype D = D(q:int, r:int, s:int, t:int)

+

+method Main()

+{

+    print D(10, 20, 30, 40);

+    print "\n";

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug113.dfy.expect b/Test/dafny4/Bug113.dfy.expect
new file mode 100644
index 00000000..c4be010e
--- /dev/null
+++ b/Test/dafny4/Bug113.dfy.expect
@@ -0,0 +1,6 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

+Program compiled successfully

+Running...

+

+D.D(10, 20, 30, 40)