From 0f4ec5c6a9e04cd49651127b31161d726841817e Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Tue, 29 Jan 2019 12:02:10 +0000 Subject: [PATCH] Rename return symbol to return' As a follow up to #3767 and to keep naming consistency between C and Java. --- jbmc/src/java_bytecode/java_entry_point.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index ce6112e22d3..6c24b213723 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -711,7 +711,7 @@ bool generate_java_start_function( return_symbol.mode=ID_java; return_symbol.is_static_lifetime=false; return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL; - return_symbol.base_name="return"; + return_symbol.base_name = "return'"; return_symbol.type = to_java_method_type(symbol.type).return_type(); symbol_table.add(return_symbol);