Skip to content

Commit 114507e

Browse files
author
Daniel Kroening
committed
use instructiont::make_X in remove_virtual_functions
This prevents duplicate initialization of instructions.
1 parent 7b3f0c1 commit 114507e

File tree

1 file changed

+18
-15
lines changed

1 file changed

+18
-15
lines changed

src/goto-programs/remove_virtual_functions.cpp

Lines changed: 18 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -228,9 +228,8 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
228228
// match any expected type:
229229
if(fallback_action==virtual_dispatch_fallback_actiont::ASSUME_FALSE)
230230
{
231-
auto newinst=new_code_calls.add_instruction(ASSUME);
232-
newinst->guard=false_exprt();
233-
newinst->source_location=vcall_source_loc;
231+
new_code_calls.add(
232+
goto_programt::make_assumption(false_exprt(), vcall_source_loc));
234233
}
235234

236235
// get initial identifier for grouping
@@ -250,29 +249,34 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
250249
// Only create one call sequence per possible target:
251250
if(insertit.second)
252251
{
253-
goto_programt::targett t1=new_code_calls.add_instruction();
254-
t1->source_location=vcall_source_loc;
255252
if(fun.symbol_expr.has_value())
256253
{
257-
// call function
258-
t1->make_function_call(code);
254+
// call function
255+
goto_programt::targett t1 = new_code_calls.add(
256+
goto_programt::make_function_call(code, vcall_source_loc));
257+
259258
create_static_function_call(
260259
t1->get_function_call(), *fun.symbol_expr, ns);
260+
261+
insertit.first->second = t1;
261262
}
262263
else
263264
{
265+
goto_programt::targett t1 = new_code_calls.add(
266+
goto_programt::make_assertion(false_exprt(), vcall_source_loc));
267+
264268
// No definition for this type; shouldn't be possible...
265-
t1->make_assertion(false_exprt());
266269
t1->source_location.set_comment(
267270
"cannot find calls for " +
268271
id2string(code.function().get(ID_identifier)) + " dispatching " +
269272
id2string(fun.class_id));
273+
274+
insertit.first->second = t1;
270275
}
271-
insertit.first->second=t1;
276+
272277
// goto final
273-
goto_programt::targett t3=new_code_calls.add_instruction();
274-
t3->source_location=vcall_source_loc;
275-
t3->make_goto(t_final, true_exprt());
278+
new_code_calls.add(
279+
goto_programt::make_goto(t_final, true_exprt(), vcall_source_loc));
276280
}
277281

278282
// Fall through to the default callee if possible:
@@ -308,9 +312,8 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
308312
}
309313
else
310314
{
311-
goto_programt::targett new_goto = new_code_gotos.add_instruction();
312-
new_goto->source_location = vcall_source_loc;
313-
new_goto->make_goto(insertit.first->second, class_id_test);
315+
new_code_gotos.add(goto_programt::make_goto(
316+
insertit.first->second, class_id_test, vcall_source_loc));
314317
}
315318
}
316319
}

0 commit comments

Comments
 (0)