Rename return symbol to return'

As a follow up to diffblue#3767 and to keep naming consistency between C and Java.
allredj · Jan 29, 2019 · ac0075f · ac0075f
1 parent 0ebe5f4
commit ac0075f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/a b/a
@@ -0,0 +1 @@
+a
diff --git 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);