Skip to content

Commit 18cb59a

Browse files
author
Daniel Kroening
committed
use new goto_programt::instructiont API
Straight-forward replacement of checked casts.
1 parent 46de172 commit 18cb59a

16 files changed

+51
-60
lines changed

‎src/goto-programs/goto_inline_class.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -343,7 +343,7 @@ void goto_inlinet::insert_function_body(
343343
if(it->function==identifier)
344344
{
345345
// don't hide assignment to lhs
346-
if(it->is_assign() && to_code_assign(it->code).lhs()==lhs)
346+
if(it->is_assign() && it->get_assign().lhs()==lhs)
347347
{
348348
}
349349
else
@@ -502,7 +502,7 @@ void goto_inlinet::get_call(
502502
{
503503
PRECONDITION(it->is_function_call());
504504

505-
const code_function_callt &call=to_code_function_call(it->code);
505+
const code_function_callt &call = it->get_function_call();
506506

507507
lhs=call.lhs();
508508
function=call.function();

‎src/goto-programs/goto_program.cpp

+12-12
Original file line numberDiff line numberDiff line change
@@ -278,14 +278,14 @@ std::list<exprt> expressions_read(
278278
break;
279279

280280
case RETURN:
281-
if(to_code_return(instruction.code).return_value().is_not_nil())
282-
dest.push_back(to_code_return(instruction.code).return_value());
281+
if(instruction.get_return().return_value().is_not_nil())
282+
dest.push_back(instruction.get_return().return_value());
283283
break;
284284

285285
case FUNCTION_CALL:
286286
{
287-
const code_function_callt &function_call=
288-
to_code_function_call(instruction.code);
287+
const code_function_callt &function_call =
288+
instruction.get_function_call();
289289
forall_expr(it, function_call.arguments())
290290
dest.push_back(*it);
291291
if(function_call.lhs().is_not_nil())
@@ -295,7 +295,7 @@ std::list<exprt> expressions_read(
295295

296296
case ASSIGN:
297297
{
298-
const code_assignt &assignment=to_code_assign(instruction.code);
298+
const code_assignt &assignment = instruction.get_assign();
299299
dest.push_back(assignment.rhs());
300300
parse_lhs_read(assignment.lhs(), dest);
301301
}
@@ -318,15 +318,15 @@ std::list<exprt> expressions_written(
318318
{
319319
case FUNCTION_CALL:
320320
{
321-
const code_function_callt &function_call=
322-
to_code_function_call(instruction.code);
321+
const code_function_callt &function_call =
322+
instruction.get_function_call();
323323
if(function_call.lhs().is_not_nil())
324324
dest.push_back(function_call.lhs());
325325
}
326326
break;
327327

328328
case ASSIGN:
329-
dest.push_back(to_code_assign(instruction.code).lhs());
329+
dest.push_back(instruction.get_assign().lhs());
330330
break;
331331

332332
default:
@@ -792,9 +792,9 @@ void goto_programt::instructiont::validate(
792792
source_location);
793793
DATA_CHECK_WITH_DIAGNOSTICS(
794794
vm,
795-
!ns.lookup(to_code_decl(code).get_identifier(), table_symbol),
795+
!ns.lookup(get_decl().get_identifier(), table_symbol),
796796
"declared symbols should be known",
797-
id2string(to_code_decl(code).get_identifier()),
797+
id2string(get_decl().get_identifier()),
798798
source_location);
799799
break;
800800
case DEAD:
@@ -805,9 +805,9 @@ void goto_programt::instructiont::validate(
805805
source_location);
806806
DATA_CHECK_WITH_DIAGNOSTICS(
807807
vm,
808-
!ns.lookup(to_code_dead(code).get_identifier(), table_symbol),
808+
!ns.lookup(get_dead().get_identifier(), table_symbol),
809809
"removed symbols should be known",
810-
id2string(to_code_dead(code).get_identifier()),
810+
id2string(get_dead().get_identifier()),
811811
source_location);
812812
break;
813813
case FUNCTION_CALL:

‎src/goto-programs/graphml_witness.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -144,10 +144,10 @@ static bool filter_out(
144144
const goto_tracet::stepst::const_iterator &prev_it,
145145
goto_tracet::stepst::const_iterator &it)
146146
{
147-
if(it->hidden &&
148-
(!it->pc->is_assign() ||
149-
to_code_assign(it->pc->code).rhs().id()!=ID_side_effect ||
150-
to_code_assign(it->pc->code).rhs().get(ID_statement)!=ID_nondet))
147+
if(
148+
it->hidden && (!it->pc->is_assign() ||
149+
it->pc->get_assign().rhs().id() != ID_side_effect ||
150+
it->pc->get_assign().rhs().get(ID_statement) != ID_nondet))
151151
return true;
152152

153153
if(!it->is_assignment() && !it->is_goto() && !it->is_assert())

‎src/goto-programs/instrument_preconditions.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ void instrument_preconditions(
101101
if(it->is_function_call())
102102
{
103103
// does the function we call have preconditions?
104-
const auto &call=to_code_function_call(it->code);
104+
const auto &call = it->get_function_call();
105105

106106
if(call.function().id()==ID_symbol)
107107
{

‎src/goto-programs/interpreter.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -746,8 +746,7 @@ void interpretert::execute_assert()
746746

747747
void interpretert::execute_function_call()
748748
{
749-
const code_function_callt &function_call=
750-
to_code_function_call(pc->code);
749+
const code_function_callt &function_call = pc->get_function_call();
751750

752751
// function to be called
753752
mp_integer address=evaluate_address(function_call.function());

‎src/goto-programs/mm_io.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ void mm_io(
4545

4646
if(it->is_assign())
4747
{
48-
auto &a=to_code_assign(it->code);
48+
auto &a = it->get_assign();
4949
collect_deref_expr(a.rhs(), deref_expr_r);
5050

5151
if(mm_io_r.is_not_nil())

‎src/goto-programs/parameter_assignments.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ void parameter_assignmentst::do_function_calls(
4242
{
4343
if(i_it->is_function_call())
4444
{
45-
code_function_callt &function_call=to_code_function_call(i_it->code);
45+
code_function_callt &function_call = i_it->get_function_call();
4646

4747
// add x=y for f(y) where x is the parameter
4848

‎src/goto-programs/remove_calls_no_body.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ bool remove_calls_no_bodyt::is_opaque_function_call(
7474
if(!target->is_function_call())
7575
return false;
7676

77-
const code_function_callt &cfc = to_code_function_call(target->code);
77+
const code_function_callt &cfc = target->get_function_call();
7878
const exprt &f = cfc.function();
7979

8080
if(f.id() != ID_symbol)
@@ -108,7 +108,7 @@ operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
108108
{
109109
if(is_opaque_function_call(it, goto_functions))
110110
{
111-
const code_function_callt &cfc = to_code_function_call(it->code);
111+
const code_function_callt &cfc = it->get_function_call();
112112
remove_call_no_body(goto_program, it, cfc.lhs(), cfc.arguments());
113113
}
114114
else

‎src/goto-programs/remove_function_pointers.cpp

+7-9
Original file line numberDiff line numberDiff line change
@@ -265,8 +265,7 @@ void remove_function_pointerst::remove_function_pointer(
265265
goto_programt &goto_program,
266266
goto_programt::targett target)
267267
{
268-
const code_function_callt &code=
269-
to_code_function_call(target->code);
268+
const code_function_callt &code = target->get_function_call();
270269

271270
const auto &function = to_dereference_expr(code.function());
272271

@@ -312,7 +311,7 @@ void remove_function_pointerst::remove_function_pointer(
312311

313312
if(functions.size()==1)
314313
{
315-
to_code_function_call(target->code).function()=*functions.cbegin();
314+
target->get_function_call().function() = *functions.cbegin();
316315
return;
317316
}
318317
}
@@ -360,7 +359,7 @@ void remove_function_pointerst::remove_function_pointer(
360359
goto_programt::targett target,
361360
const functionst &functions)
362361
{
363-
const code_function_callt &code = to_code_function_call(target->code);
362+
const code_function_callt &code = target->get_function_call();
364363

365364
const exprt &function = code.function();
366365
const exprt &pointer = to_dereference_expr(function).pointer();
@@ -381,12 +380,12 @@ void remove_function_pointerst::remove_function_pointer(
381380
// call function
382381
goto_programt::targett t1=new_code_calls.add_instruction();
383382
t1->make_function_call(code);
384-
to_code_function_call(t1->code).function()=fun;
383+
t1->get_function_call().function() = fun;
385384

386385
// the signature of the function might not match precisely
387-
fix_argument_types(to_code_function_call(t1->code));
386+
fix_argument_types(t1->get_function_call());
388387

389-
fix_return_type(to_code_function_call(t1->code), new_code_calls);
388+
fix_return_type(t1->get_function_call(), new_code_calls);
390389
// goto final
391390
goto_programt::targett t3=new_code_calls.add_instruction();
392391
t3->make_goto(t_final, true_exprt());
@@ -474,8 +473,7 @@ bool remove_function_pointerst::remove_function_pointers(
474473
Forall_goto_program_instructions(target, goto_program)
475474
if(target->is_function_call())
476475
{
477-
const code_function_callt &code=
478-
to_code_function_call(target->code);
476+
const code_function_callt &code = target->get_function_call();
479477

480478
if(code.function().id()==ID_dereference)
481479
{

‎src/goto-programs/remove_returns.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ void remove_returnst::do_function_calls(
149149
{
150150
if(i_it->is_function_call())
151151
{
152-
code_function_callt &function_call=to_code_function_call(i_it->code);
152+
code_function_callt &function_call = i_it->get_function_call();
153153

154154
INVARIANT(
155155
function_call.function().id() == ID_symbol,
@@ -357,7 +357,7 @@ bool remove_returnst::restore_returns(
357357
{
358358
if(i_it->is_assign())
359359
{
360-
code_assignt &assign=to_code_assign(i_it->code);
360+
code_assignt &assign = i_it->get_assign();
361361
if(assign.lhs().id()!=ID_symbol ||
362362
to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id)
363363
continue;
@@ -386,7 +386,7 @@ void remove_returnst::undo_function_calls(
386386
{
387387
if(i_it->is_function_call())
388388
{
389-
code_function_callt &function_call=to_code_function_call(i_it->code);
389+
code_function_callt &function_call = i_it->get_function_call();
390390

391391
// ignore function pointers
392392
if(function_call.function().id()!=ID_symbol)
@@ -412,7 +412,7 @@ void remove_returnst::undo_function_calls(
412412
if(!next->is_assign())
413413
continue;
414414

415-
const code_assignt &assign=to_code_assign(next->code);
415+
const code_assignt &assign = next->get_assign();
416416

417417
if(assign.rhs().id()!=ID_symbol)
418418
continue;

‎src/goto-programs/remove_unused_functions.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ void find_used_functions(
7575
{
7676
if(it->type==FUNCTION_CALL)
7777
{
78-
const code_function_callt &call = to_code_function_call(it->code);
78+
const code_function_callt &call = it->get_function_call();
7979

8080
const irep_idt &identifier =
8181
to_symbol_expr(call.function()).get_identifier();

‎src/goto-programs/remove_virtual_functions.cpp

+5-10
Original file line numberDiff line numberDiff line change
@@ -83,8 +83,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
8383
goto_programt &goto_program,
8484
goto_programt::targett target)
8585
{
86-
const code_function_callt &code=
87-
to_code_function_call(target->code);
86+
const code_function_callt &code = target->get_function_call();
8887

8988
const exprt &function=code.function();
9089
INVARIANT(
@@ -150,8 +149,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
150149
INVARIANT(
151150
target->is_function_call(),
152151
"remove_virtual_function must target a FUNCTION_CALL instruction");
153-
const code_function_callt &code=
154-
to_code_function_call(target->code);
152+
const code_function_callt &code = target->get_function_call();
155153

156154
goto_programt::targett next_target = std::next(target);
157155

@@ -174,9 +172,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
174172
else
175173
{
176174
create_static_function_call(
177-
to_code_function_call(target->code),
178-
*functions.front().symbol_expr,
179-
ns);
175+
target->get_function_call(), *functions.front().symbol_expr, ns);
180176
}
181177
return next_target;
182178
}
@@ -242,7 +238,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
242238
// call function
243239
t1->make_function_call(code);
244240
create_static_function_call(
245-
to_code_function_call(t1->code), *fun.symbol_expr, ns);
241+
t1->get_function_call(), *fun.symbol_expr, ns);
246242
}
247243
else
248244
{
@@ -530,8 +526,7 @@ bool remove_virtual_functionst::remove_virtual_functions(
530526
{
531527
if(target->is_function_call())
532528
{
533-
const code_function_callt &code=
534-
to_code_function_call(target->code);
529+
const code_function_callt &code = target->get_function_call();
535530

536531
if(code.function().id()==ID_virtual_function)
537532
{

‎src/goto-programs/replace_calls.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ void replace_callst::operator()(
7070
if(!ins.is_function_call())
7171
continue;
7272

73-
code_function_callt &cfc = to_code_function_call(ins.code);
73+
code_function_callt &cfc = ins.get_function_call();
7474
exprt &function = cfc.function();
7575

7676
PRECONDITION(function.id() == ID_symbol);
@@ -100,7 +100,7 @@ void replace_callst::operator()(
100100
goto_programt::const_targett next_it = std::next(it);
101101
if(next_it != goto_program.instructions.end() && next_it->is_assign())
102102
{
103-
const code_assignt &ca = to_code_assign(next_it->code);
103+
const code_assignt &ca = next_it->get_assign();
104104
const exprt &rhs = ca.rhs();
105105

106106
INVARIANT(

‎src/goto-programs/slice_global_inits.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ void slice_global_inits(goto_modelt &goto_model)
8585
{
8686
if(i_it->is_assign())
8787
{
88-
const code_assignt &code_assign=to_code_assign(i_it->code);
88+
const code_assignt &code_assign = i_it->get_assign();
8989
const symbol_exprt &symbol_expr=to_symbol_expr(code_assign.lhs());
9090
const irep_idt id=symbol_expr.get_identifier();
9191

‎src/goto-programs/string_abstraction.cpp

+6-6
Original file line numberDiff line numberDiff line change
@@ -249,8 +249,8 @@ void string_abstractiont::declare_define_locals(goto_programt &dest)
249249
if(it->is_decl())
250250
// same name may exist several times due to inlining, make sure the first
251251
// declaration is used
252-
available_decls.insert(std::make_pair(
253-
to_code_decl(it->code).get_identifier(), it));
252+
available_decls.insert(
253+
std::make_pair(it->get_decl().get_identifier(), it));
254254

255255
// declare (and, if necessary, define) locals
256256
for(const auto &l : locals)
@@ -501,7 +501,7 @@ goto_programt::targett string_abstractiont::abstract_assign(
501501
goto_programt &dest,
502502
goto_programt::targett target)
503503
{
504-
code_assignt &assign=to_code_assign(target->code);
504+
code_assignt &assign = target->get_assign();
505505

506506
exprt &lhs=assign.lhs();
507507
exprt &rhs=assign.rhs();
@@ -527,7 +527,7 @@ goto_programt::targett string_abstractiont::abstract_assign(
527527
void string_abstractiont::abstract_function_call(
528528
goto_programt::targett target)
529529
{
530-
code_function_callt &call=to_code_function_call(target->code);
530+
code_function_callt &call = target->get_function_call();
531531
code_function_callt::argumentst &arguments=call.arguments();
532532
code_function_callt::argumentst str_args;
533533

@@ -1060,7 +1060,7 @@ goto_programt::targett string_abstractiont::abstract_pointer_assign(
10601060
goto_programt &dest,
10611061
goto_programt::targett target)
10621062
{
1063-
code_assignt &assign=to_code_assign(target->code);
1063+
code_assignt &assign = target->get_assign();
10641064

10651065
exprt &lhs=assign.lhs();
10661066
exprt rhs=assign.rhs();
@@ -1105,7 +1105,7 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
11051105
goto_programt &dest,
11061106
goto_programt::targett target)
11071107
{
1108-
code_assignt &assign=to_code_assign(target->code);
1108+
code_assignt &assign = target->get_assign();
11091109

11101110
exprt &lhs=assign.lhs();
11111111
exprt *rhsp=&(assign.rhs());

‎src/goto-programs/string_instrumentation.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -222,8 +222,7 @@ void string_instrumentationt::do_function_call(
222222
goto_programt &dest,
223223
goto_programt::targett target)
224224
{
225-
code_function_callt &call=
226-
to_code_function_call(target->code);
225+
code_function_callt &call = target->get_function_call();
227226
exprt &function=call.function();
228227
// const exprt &lhs=call.lhs();
229228

0 commit comments

Comments
 (0)