From 0e4176d2383d77459df5731c1abb7e471769c383 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 30 Jun 2017 17:06:26 +0100 Subject: [PATCH 1/2] Fix modes in java entry point code --- src/java_bytecode/java_entry_point.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index bb7e488c8a5..6f6ebd5f149 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -522,7 +522,7 @@ bool java_entry_point( if(to_code_type(symbol.type).return_type()!=empty_typet()) { auxiliary_symbolt return_symbol; - return_symbol.mode=ID_C; + return_symbol.mode=ID_java; return_symbol.is_static_lifetime=false; return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL; return_symbol.base_name="return"; @@ -536,7 +536,7 @@ bool java_entry_point( { // add the exceptional return value auxiliary_symbolt exc_symbol; - exc_symbol.mode=ID_C; + exc_symbol.mode=ID_java; exc_symbol.is_static_lifetime=true; exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX; exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX; From 5409f56310502de3edc64158830f8e0811857a55 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 30 Jun 2017 17:52:05 +0100 Subject: [PATCH 2/2] Add missing header guard endif comment --- src/java_bytecode/java_entry_point.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index c05a78b0689..9437ba65d70 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -34,4 +34,4 @@ main_function_resultt get_main_symbol( message_handlert &, bool allow_no_body=false); -#endif +#endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H