Skip to content

Commit 6a18c24

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#1079 from peterschrammel/bugfix/java-entry-point-modes
Fix modes in java entry point code
2 parents b63547f + 5409f56 commit 6a18c24

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

src/java_bytecode/java_entry_point.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -522,7 +522,7 @@ bool java_entry_point(
522522
if(to_code_type(symbol.type).return_type()!=empty_typet())
523523
{
524524
auxiliary_symbolt return_symbol;
525-
return_symbol.mode=ID_C;
525+
return_symbol.mode=ID_java;
526526
return_symbol.is_static_lifetime=false;
527527
return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
528528
return_symbol.base_name="return";
@@ -536,7 +536,7 @@ bool java_entry_point(
536536
{
537537
// add the exceptional return value
538538
auxiliary_symbolt exc_symbol;
539-
exc_symbol.mode=ID_C;
539+
exc_symbol.mode=ID_java;
540540
exc_symbol.is_static_lifetime=true;
541541
exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX;
542542
exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX;

src/java_bytecode/java_entry_point.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -34,4 +34,4 @@ main_function_resultt get_main_symbol(
3434
message_handlert &,
3535
bool allow_no_body=false);
3636

37-
#endif
37+
#endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H

0 commit comments

Comments
 (0)