Skip to content

Commit a7a84c1

Browse files
Fix base_name of argc' symbol to match its name
1 parent b837116 commit a7a84c1

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -237,7 +237,7 @@ bool generate_ansi_c_start_function(
237237
return_symbol.mode=ID_C;
238238
return_symbol.is_static_lifetime=false;
239239
return_symbol.name="return'";
240-
return_symbol.base_name="return'";
240+
return_symbol.base_name = "return'";
241241
return_symbol.type=to_code_type(symbol.type).return_type();
242242

243243
symbol_table.add(return_symbol);
@@ -260,7 +260,7 @@ bool generate_ansi_c_start_function(
260260
{
261261
symbolt argc_symbol;
262262

263-
argc_symbol.base_name = "argc";
263+
argc_symbol.base_name = "argc'";
264264
argc_symbol.name = "argc'";
265265
argc_symbol.type = signed_int_type();
266266
argc_symbol.is_static_lifetime = true;

0 commit comments

Comments
 (0)