diff --git a/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 444d87c108d..039f6de763a 100644 --- a/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -85,7 +85,7 @@ class patternt /// \return Assigns parameter names (side-effects on `ftype`) to function stub /// parameters, which are initially nameless as method conversion hasn't /// happened. Also creates symbols in `symbol_table`. -static void assign_parameter_names( +void assign_parameter_names( code_typet &ftype, const irep_idt &name_prefix, symbol_table_baset &symbol_table) diff --git a/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.h index 4fa21fc85dd..47cdbb0680b 100644 --- a/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -46,4 +46,9 @@ void java_bytecode_convert_method_lazy( symbol_tablet &symbol_table, message_handlert &); +void assign_parameter_names( + code_typet &ftype, + const irep_idt &name_prefix, + symbol_table_baset &symbol_table); + #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H diff --git a/src/driver/sec_driver_parse_options.cpp b/src/driver/sec_driver_parse_options.cpp index e953bf2399d..9d1ce1f6702 100644 --- a/src/driver/sec_driver_parse_options.cpp +++ b/src/driver/sec_driver_parse_options.cpp @@ -32,6 +32,7 @@ #include #include +#include #include #include #include @@ -659,17 +660,31 @@ bool sec_driver_parse_optionst::generate_function_body( goto_functiont &function, bool body_available) { + const symbolt *symbol = symbol_table.lookup(function_name); + // Provide a simple stub implementation for any function we don't have a // bytecode implementation for: if(body_available || !can_generate_function_body(function_name)) { - const symbolt *symbol = symbol_table.lookup(function_name); if(symbol == nullptr || !symbol->type.get_bool(ID_C_abstract)) return false; } - if(symbol_table.lookup_ref(function_name).mode == ID_java) + if(symbol->mode == ID_java) { + code_typet code_type = to_code_type(symbol->type); + + // Note this may invalidate pointer `symbol` by adding to the symtab, so: + symbol = nullptr; + + if( + code_type.parameters().size() != 0 && + code_type.parameters()[0].get_identifier().empty()) + { + assign_parameter_names(code_type, function_name, symbol_table); + symbol_table.get_writeable_ref(function_name).type = code_type; + } + java_generate_simple_method_stub( function_name, symbol_table,