Skip to content

Commit 1dff4c3

Browse files
committed
Java object factory: pass function ID to factory routine
Previously this was accidentally dropped when used from the goto_functionst entry point.
1 parent d48e840 commit 1dff4c3

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

jbmc/src/java_bytecode/convert_java_nondet.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -168,9 +168,13 @@ void convert_nondet(
168168
goto_programt &goto_program,
169169
symbol_table_baset &symbol_table,
170170
message_handlert &message_handler,
171-
const java_object_factory_parameterst &object_factory_parameters,
171+
const java_object_factory_parameterst &user_object_factory_parameters,
172172
const irep_idt &mode)
173173
{
174+
java_object_factory_parameterst
175+
object_factory_parameters = user_object_factory_parameters;
176+
object_factory_parameters.function_id = function_identifier;
177+
174178
bool changed = false;
175179
auto instruction_iterator = goto_program.instructions.begin();
176180

@@ -200,14 +204,12 @@ void convert_nondet(
200204
const java_object_factory_parameterst &object_factory_parameters,
201205
const irep_idt &mode)
202206
{
203-
java_object_factory_parameterst parameters = object_factory_parameters;
204-
parameters.function_id = function.get_function_id();
205207
convert_nondet(
206208
function.get_function_id(),
207209
function.get_goto_function().body,
208210
function.get_symbol_table(),
209211
message_handler,
210-
parameters,
212+
object_factory_parameters,
211213
mode);
212214

213215
function.compute_location_numbers();
@@ -227,8 +229,6 @@ void convert_nondet(
227229

228230
if(symbol.mode==ID_java)
229231
{
230-
java_object_factory_parameterst parameters = object_factory_parameters;
231-
parameters.function_id = f_it.first;
232232
convert_nondet(
233233
f_it.first,
234234
f_it.second.body,

0 commit comments

Comments
 (0)