diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 49b621aed89..45211a6f022 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "java_bytecode_convert_method.h" #include "bytecode_info.h" @@ -701,7 +702,12 @@ codet java_bytecode_convert_methodt::convert_instructions( if(return_type.id()!=ID_empty) { results.resize(1); - results[0]=nil_exprt(); + results[0]= + zero_initializer( + return_type, + i_it->source_location, + namespacet(symbol_table), + get_message_handler()); } } else if(statement=="invokeinterface" ||