diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 5c3beafc357..1597868caf2 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -203,7 +203,7 @@ exprt::operandst java_build_arguments( !assume_init_pointers_not_null && !is_main && !is_this; object_factory_parameterst parameters = object_factory_parameters; - parameters.function_id = function.name; + parameters.function_id = goto_functionst::entry_point(); // generate code to allocate and non-deterministicaly initialize the // argument