@@ -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,39 @@ 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 parameter's base name
483+ // or with another local variable's base name. If so, rename the local variable to avoid collision.
484+ const symbolt *local_symbol_ptr = nullptr ;
485+ if (!ns.lookup (symbol.get_identifier (), local_symbol_ptr))
486+ {
487+ const symbolt &local_symbol = *local_symbol_ptr;
488+ irep_idt base_name = local_symbol.base_name ;
489+
490+ if (
491+ !base_name.empty () &&
492+ (param_names.find (base_name) != param_names.end () ||
493+ used_local_names.find (base_name) != used_local_names.end ()))
494+ {
495+ // Generate a unique base name by appending a suffix
496+ irep_idt new_base_name;
497+ unsigned suffix = 1 ;
498+ do
499+ {
500+ new_base_name = id2string (base_name) + " $" + std::to_string (suffix);
501+ ++suffix;
502+ } while (param_names.find (new_base_name) != param_names.end () ||
503+ used_local_names.find (new_base_name) != used_local_names.end ());
504+
505+ // Update the symbol in the symbol table with the new base name
506+ symbolt &sym = symbol_table.get_writeable_ref (symbol.get_identifier ());
507+ sym.base_name = new_base_name;
508+ base_name = new_base_name;
509+ }
510+
511+ // Track this local variable's base name
512+ used_local_names.insert (base_name);
513+ }
514+
458515 goto_programt::const_targett next=target;
459516 ++next;
460517 CHECK_RETURN (next != goto_program.instructions .end ());
0 commit comments