diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index c655eb7d02b..b63d5923e5f 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -877,14 +877,7 @@ bool java_bytecode_languaget::convert_single_method( bool java_bytecode_languaget::final(symbol_table_baset &symbol_table) { PRECONDITION(language_options_initialized); - - return recreate_initialize( - symbol_table, - main_class, - get_message_handler(), - assume_inputs_non_null, - object_factory_parameters, - get_pointer_type_selector()); + return false; } void java_bytecode_languaget::show_parse(std::ostream &out) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index e8e2343937d..2f2242c4424 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -455,48 +455,6 @@ bool java_entry_point( pointer_type_selector); } -/// Creates the initialize methods again taking account of symbols added to the -/// symbol table during instantiation of lazy methods since they were first -/// created, -/// \param symbol_table: global symbol table containing symbols to initialize -/// \param main_class: the class containing the "main" entry point -/// \param message_handler: message_handlert for logging -/// \param assume_init_pointers_not_null: specifies behaviour for -/// java_static_lifetime_init -/// \param object_factory_parameters: specifies behaviour for -/// java_static_lifetime_init -/// \param pointer_type_selector: specifies behaviour for -/// java_static_lifetime_init -bool recreate_initialize( - symbol_table_baset &symbol_table, - const irep_idt &main_class, - message_handlert &message_handler, - bool assume_init_pointers_not_null, - const object_factory_parameterst &object_factory_parameters, - const select_pointer_typet &pointer_type_selector) -{ - messaget message(message_handler); - main_function_resultt res= - get_main_symbol(symbol_table, main_class, message_handler); - if(res.status!=main_function_resultt::Success) - { - // No initialization was originally created (yikes!) so we can't recreate - // it now - return res.status==main_function_resultt::Error; - } - - create_initialize(symbol_table); - - java_static_lifetime_init( - symbol_table, - res.main_function.location, - assume_init_pointers_not_null, - object_factory_parameters, - pointer_type_selector); - - return false; -} - /// Generate a _start function for a specific function. See /// java_entry_point for more details. /// \param symbol: The symbol representing the function to call diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index 98495c72a5a..399078ee2f8 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -73,12 +73,4 @@ bool generate_java_start_function( const object_factory_parameterst& object_factory_parameters, const select_pointer_typet &pointer_type_selector); -bool recreate_initialize( - symbol_table_baset &symbol_table, - const irep_idt &main_class, - message_handlert &message_handler, - bool assume_init_pointers_not_null, - const object_factory_parameterst &object_factory_parameters, - const select_pointer_typet &pointer_type_selector); - #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H