@@ -37,6 +37,9 @@ void goto_program2codet::operator()()
3737 // gather variable scope information
3838 build_dead_map ();
3939
40+ // gather function parameter names to avoid collision with local variables
41+ build_param_names ();
42+
4043 // see whether var args are in use, identify va_list symbol
4144 scan_for_varargs ();
4245
@@ -101,6 +104,27 @@ void goto_program2codet::build_dead_map()
101104 }
102105}
103106
107+ void goto_program2codet::build_param_names ()
108+ {
109+ param_names.clear ();
110+
111+ // Get function parameters from the symbol table
112+ const symbolt *func_symbol = nullptr ;
113+ if (!ns.lookup (func_name, func_symbol) && func_symbol->type .id () == ID_code)
114+ {
115+ const code_typet &code_type = to_code_type (func_symbol->type );
116+ const code_typet::parameterst ¶meters = code_type.parameters ();
117+
118+ // Store the base names of parameters (as they appear in C output)
119+ for (const auto ¶m : parameters)
120+ {
121+ const irep_idt ¶m_base_name = param.get_base_name ();
122+ if (!param_base_name.empty ())
123+ param_names.insert (param_base_name);
124+ }
125+ }
126+ }
127+
104128void goto_program2codet::scan_for_varargs ()
105129{
106130 va_list_expr.clear ();
@@ -455,6 +479,40 @@ goto_programt::const_targett goto_program2codet::convert_decl(
455479 code_frontend_declt d = code_frontend_declt{target->decl_symbol ()};
456480 symbol_exprt &symbol = d.symbol ();
457481
482+ // Check if the local variable's base name conflicts with a function
483+ // parameter's base name or with another local variable's base name. If so,
484+ // rename the local variable to avoid collision.
485+ const symbolt *local_symbol_ptr = nullptr ;
486+ if (!ns.lookup (symbol.get_identifier (), local_symbol_ptr))
487+ {
488+ const symbolt &local_symbol = *local_symbol_ptr;
489+ irep_idt base_name = local_symbol.base_name ;
490+
491+ if (
492+ !base_name.empty () &&
493+ (param_names.find (base_name) != param_names.end () ||
494+ used_local_names.find (base_name) != used_local_names.end ()))
495+ {
496+ // Generate a unique base name by appending a suffix
497+ irep_idt new_base_name;
498+ unsigned suffix = 1 ;
499+ do
500+ {
501+ new_base_name = id2string (base_name) + " $" + std::to_string (suffix);
502+ ++suffix;
503+ } while (param_names.find (new_base_name) != param_names.end () ||
504+ used_local_names.find (new_base_name) != used_local_names.end ());
505+
506+ // Update the symbol in the symbol table with the new base name
507+ symbolt &sym = symbol_table.get_writeable_ref (symbol.get_identifier ());
508+ sym.base_name = new_base_name;
509+ base_name = new_base_name;
510+ }
511+
512+ // Track this local variable's base name
513+ used_local_names.insert (base_name);
514+ }
515+
458516 goto_programt::const_targett next=target;
459517 ++next;
460518 CHECK_RETURN (next != goto_program.instructions .end ());
0 commit comments