Skip to content

Commit 0f4ec5c

Browse files
author
Joel Allred
committed
Rename return symbol to return'
As a follow up to #3767 and to keep naming consistency between C and Java.
1 parent 0ebe5f4 commit 0f4ec5c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -711,7 +711,7 @@ bool generate_java_start_function(
711711
return_symbol.mode=ID_java;
712712
return_symbol.is_static_lifetime=false;
713713
return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
714-
return_symbol.base_name="return";
714+
return_symbol.base_name = "return'";
715715
return_symbol.type = to_java_method_type(symbol.type).return_type();
716716

717717
symbol_table.add(return_symbol);

0 commit comments

Comments
 (0)