Fix goto-instrument --dump-c parameter/local variable name collision

regression/goto-instrument/dump-param-local-collision/main.c

@@ -0,0 +1,25 @@
+// Test case for parameter/local variable name collision in goto-instrument --dump-c
+// This should generate valid C code with renamed local variables
+
+int help(int x)
+{
+  unsigned int x; // Should be renamed to x$1 in output
+  x = 42;
+  return (int)x;
+}
+
+int test_two_params(int y, int z)
+{
+  int y; // Should be renamed to y$1
+  int z; // Should be renamed to z$1
+  y = 10;
+  z = 20;
+  return y + z;
+}
+
+int main()
+{
+  int result = help(1);
+  result += test_two_params(5, 6);
+  return result;
+}

regression/goto-instrument/dump-param-local-collision/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test ensures that goto-instrument --dump-c produces valid C code when a
+local variable has the same name as a function parameter. Previously, this
+would generate invalid C code like:
+  int help(int x) { unsigned int x; }
+which causes a compilation error. The fix renames the local variable to avoid
+the collision, e.g.:
+  int help(int x) { unsigned int x$1; }
+
+The generated C code should be valid and compilable.
+
+Related to issue #6268 (similar to issue #6242 but for a different case).

src/goto-instrument/goto_program2code.cpp

@@ -37,6 +37,10 @@ void goto_program2codet::operator()()
   // gather variable scope information
   build_dead_map();
 
+  // gather function parameter names to avoid collision with local variables
+  build_param_names();
+  used_local_names.clear();
+
   // see whether var args are in use, identify va_list symbol
   scan_for_varargs();
 
@@ -101,6 +105,27 @@ void goto_program2codet::build_dead_map()
   }
 }
 
+void goto_program2codet::build_param_names()
+{
+  param_names.clear();
+
+  // Get function parameters from the symbol table
+  const symbolt *func_symbol = nullptr;
+  if(!ns.lookup(func_name, func_symbol) && func_symbol->type.id() == ID_code)
+  {
+    const code_typet &code_type = to_code_type(func_symbol->type);
+    const code_typet::parameterst &parameters = code_type.parameters();
+
+    // Store the base names of parameters (as they appear in C output)
+    for(const auto &param : parameters)
+    {
+      const irep_idt &param_base_name = param.get_base_name();
+      if(!param_base_name.empty())
+        param_names.insert(param_base_name);
+    }
+  }
+}
+
 void goto_program2codet::scan_for_varargs()
 {
   va_list_expr.clear();
@@ -455,6 +480,40 @@ goto_programt::const_targett goto_program2codet::convert_decl(
   code_frontend_declt d = code_frontend_declt{target->decl_symbol()};
   symbol_exprt &symbol = d.symbol();
 
+  // Check if the local variable's base name conflicts with a function
+  // parameter's base name or with another local variable's base name. If so,
+  // rename the local variable to avoid collision.
+  const symbolt *local_symbol_ptr = nullptr;
+  if(!ns.lookup(symbol.get_identifier(), local_symbol_ptr))
+  {
+    const symbolt &local_symbol = *local_symbol_ptr;
+    irep_idt base_name = local_symbol.base_name;
+
+    if(
+      !base_name.empty() &&
+      (param_names.find(base_name) != param_names.end() ||
+       used_local_names.find(base_name) != used_local_names.end()))
+    {
+      // Generate a unique base name by appending a suffix
+      irep_idt new_base_name;
+      unsigned suffix = 1;
+      do
+      {
+        new_base_name = id2string(base_name) + "$" + std::to_string(suffix);
+        ++suffix;
+      } while(param_names.find(new_base_name) != param_names.end() ||
+              used_local_names.find(new_base_name) != used_local_names.end());
+
+      // Update the symbol in the symbol table with the new base name
+      symbolt &sym = symbol_table.get_writeable_ref(symbol.get_identifier());
+      sym.base_name = new_base_name;
+      base_name = new_base_name;
+    }
+
+    // Track this local variable's base name
+    used_local_names.insert(base_name);
+  }
+
   goto_programt::const_targett next=target;
   ++next;
   CHECK_RETURN(next != goto_program.instructions.end());

src/goto-instrument/goto_program2code.h

@@ -81,7 +81,7 @@ class goto_program2codet
   void operator()();
 
 protected:
-  const irep_idt &func_name;
+  const irep_idt func_name;
   const goto_programt &goto_program;
   symbol_tablet &symbol_table;
   const namespacet ns;
@@ -100,11 +100,14 @@ class goto_program2codet
   std::unordered_set<irep_idt> local_static_set;
   std::unordered_set<irep_idt> type_names_set;
   std::unordered_set<irep_idt> const_removed;
+  std::unordered_set<irep_idt> param_names;
+  std::unordered_set<irep_idt> used_local_names;
 
   void copy_source_location(goto_programt::const_targett, codet &dst);
 
   void build_loop_map();
   void build_dead_map();
+  void build_param_names();
   void scan_for_varargs();
 
   void cleanup_code(codet &code, const irep_idt parent_stmt);