From 15a45445f47fac7062f1d227faa0d17789909527 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 5 Oct 2020 17:13:35 +0200
Subject: [PATCH] [typing] fix issue when renaming local function

Fixes #946
---
 src/kernel_internals/typing/cabs2cil.ml       | 58 +++++++++++--------
 tests/syntax/local-variable.i                 |  7 +++
 tests/syntax/oracle/local-variable.res.oracle | 15 +++++
 3 files changed, 55 insertions(+), 25 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 01a5dcd2ee2..89290cbc881 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1125,31 +1125,39 @@ let alphaConvertVarAndAddToEnv addtoenv vi =
       vi
     else begin
       if vi.vglob then begin
-        (* Perhaps this is because we have seen a static local which happened
-         * to get the name that we later want to use for a global. *)
-        try
-          let static_local_vi = H.find staticLocals vi.vname in
-          H.remove staticLocals vi.vname;
-          (* Use the new name for the static local *)
-          static_local_vi.vname <- newname;
-          (* And continue using the last one *)
-          vi
-        with Not_found -> begin
-            (* Or perhaps we have seen a typedef which stole our name. This is
-               possible because typedefs use the same name space *)
-            try
-              let typedef_ti = H.find typedefs vi.vname in
-              H.remove typedefs vi.vname;
-              (* Use the new name for the typedef instead *)
-              typedef_ti.tname <- newname;
-              (* And continue using the last name *)
-              vi
-            with Not_found ->
-              abort_context
-                "It seems that we would need to rename global %s (to %s) \
-                 because of previous occurrence at %a"
-                vi.vname newname Cil_printer.pp_location oldloc;
-          end
+        (* if a purely local variable stole our name, force it to be renamed.*)
+        let local =
+          List.find_opt
+            (fun x -> x.vname = vi.vname) !currentFunctionFDEC.slocals
+        in
+        match local with
+        | Some local -> local.vname <- newname; vi
+        | None ->
+          (* Perhaps this is because we have seen a static local which happened
+           * to get the name that we later want to use for a global. *)
+          try
+            let static_local_vi = H.find staticLocals vi.vname in
+            H.remove staticLocals vi.vname;
+            (* Use the new name for the static local *)
+            static_local_vi.vname <- newname;
+            (* And continue using the last one *)
+            vi
+          with Not_found -> begin
+              (* Or perhaps we have seen a typedef which stole our name. This is
+                 possible because typedefs use the same name space *)
+              try
+                let typedef_ti = H.find typedefs vi.vname in
+                H.remove typedefs vi.vname;
+                (* Use the new name for the typedef instead *)
+                typedef_ti.tname <- newname;
+                (* And continue using the last name *)
+                vi
+              with Not_found ->
+                abort_context
+                  "It seems that we would need to rename global %s (to %s) \
+                   because of previous occurrence at %a"
+                  vi.vname newname Cil_printer.pp_location oldloc;
+            end
       end else copyVarinfo vi newname
     end
   in
diff --git a/tests/syntax/local-variable.i b/tests/syntax/local-variable.i
index e1f1524ec86..69b1f471472 100644
--- a/tests/syntax/local-variable.i
+++ b/tests/syntax/local-variable.i
@@ -19,3 +19,10 @@ void h (int i) {
 
 int c;
 int g() { return 1 || (-1L || g(), c); }
+
+int nop(void) {
+  { int loc_var; }
+  { int loc_var (void);
+    return loc_var();
+  }
+}
diff --git a/tests/syntax/oracle/local-variable.res.oracle b/tests/syntax/oracle/local-variable.res.oracle
index 4fb72f25b39..f0fd9cdfe14 100644
--- a/tests/syntax/oracle/local-variable.res.oracle
+++ b/tests/syntax/oracle/local-variable.res.oracle
@@ -33,4 +33,19 @@ int g(void)
   return __retres;
 }
 
+int loc_var(void);
+
+int nop(void)
+{
+  {
+    int loc_var_0;
+    
+  }
+  {
+    int tmp;
+    tmp = loc_var();
+    return tmp;
+  }
+}
+
 
-- 
GitLab