From e2bab8d4be0805bf22f7295be2014a39d1e18535 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 3 Dec 2015 11:14:28 -0800
Subject: Fix issue 113. Make sure the tempVar name used in ToString() method
 doesn't collide with the names of its formals.

---
 Source/Dafny/Compiler.cs | 32 ++++++++++++++++++++++++++------
 1 file changed, 26 insertions(+), 6 deletions(-)

(limited to 'Source')

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);
 
-- 
cgit v1.2.3