Skip to content

Commit 054ac09

Browse files
authored
Merge pull request #4000 from diffblue/use_make_X
Use goto_programt::make_X factories in goto_convert
2 parents bcaff7d + 20a908d commit 054ac09

File tree

2 files changed

+38
-66
lines changed

2 files changed

+38
-66
lines changed

src/goto-programs/goto_convert.cpp

Lines changed: 31 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -531,9 +531,7 @@ void goto_convertt::convert(
531531
// make sure dest is never empty
532532
if(dest.instructions.empty())
533533
{
534-
dest.add_instruction(SKIP);
535-
dest.instructions.back().code.make_nil();
536-
dest.instructions.back().source_location=code.source_location();
534+
dest.add(goto_programt::make_skip(code.source_location()));
537535
}
538536
}
539537

@@ -1033,9 +1031,8 @@ void goto_convertt::convert_while(
10331031

10341032
// do the z label
10351033
goto_programt tmp_z;
1036-
goto_programt::targett z=tmp_z.add_instruction();
1037-
z->make_skip();
1038-
z->source_location=source_location;
1034+
goto_programt::targett z =
1035+
tmp_z.add(goto_programt::make_skip(source_location));
10391036

10401037
goto_programt tmp_branch;
10411038
generate_conditional_branch(
@@ -1107,9 +1104,8 @@ void goto_convertt::convert_dowhile(
11071104

11081105
// do the z label
11091106
goto_programt tmp_z;
1110-
goto_programt::targett z=tmp_z.add_instruction();
1111-
z->make_skip();
1112-
z->source_location=code.source_location();
1107+
goto_programt::targett z =
1108+
tmp_z.add(goto_programt::make_skip(code.source_location()));
11131109

11141110
// do the x label
11151111
goto_programt::targett x;
@@ -1187,8 +1183,7 @@ void goto_convertt::convert_switch(
11871183

11881184
// we first add a 'location' node for the switch statement,
11891185
// which would otherwise not be recorded
1190-
dest.add_instruction()->make_location(
1191-
code.source_location());
1186+
dest.add(goto_programt::make_location(code.source_location()));
11921187

11931188
// get the location of the end of the body, but
11941189
// default to location of switch, if none
@@ -1208,9 +1203,8 @@ void goto_convertt::convert_switch(
12081203

12091204
// do the z label
12101205
goto_programt tmp_z;
1211-
goto_programt::targett z=tmp_z.add_instruction();
1212-
z->make_skip();
1213-
z->source_location=body_end_location;
1206+
goto_programt::targett z =
1207+
tmp_z.add(goto_programt::make_skip(body_end_location));
12141208

12151209
// set the new targets -- continue stays as is
12161210
targets.set_break(z);
@@ -1250,17 +1244,12 @@ void goto_convertt::convert_switch(
12501244
case_number++;
12511245
guard_expr.add_source_location()=source_location;
12521246

1253-
goto_programt::targett x=tmp_cases.add_instruction();
1254-
x->make_goto(case_pair.first);
1255-
x->guard.swap(guard_expr);
1256-
x->source_location=source_location;
1247+
tmp_cases.add(goto_programt::make_goto(
1248+
case_pair.first, std::move(guard_expr), source_location));
12571249
}
12581250

1259-
{
1260-
goto_programt::targett d_jump=tmp_cases.add_instruction();
1261-
d_jump->make_goto(targets.default_target);
1262-
d_jump->source_location=targets.default_target->source_location;
1263-
}
1251+
tmp_cases.add(goto_programt::make_goto(
1252+
targets.default_target, targets.default_target->source_location));
12641253

12651254
dest.destructive_append(sideeffects);
12661255
dest.destructive_append(tmp_cases);
@@ -1284,9 +1273,8 @@ void goto_convertt::convert_break(
12841273
code.source_location(), targets.break_stack_size, dest, mode);
12851274

12861275
// add goto
1287-
goto_programt::targett t=dest.add_instruction();
1288-
t->make_goto(targets.break_target);
1289-
t->source_location=code.source_location();
1276+
dest.add(
1277+
goto_programt::make_goto(targets.break_target, code.source_location()));
12901278
}
12911279

12921280
void goto_convertt::convert_return(
@@ -1329,10 +1317,7 @@ void goto_convertt::convert_return(
13291317
new_code.find_source_location());
13301318

13311319
// Now add a return node to set the return value.
1332-
goto_programt::targett t=dest.add_instruction();
1333-
t->make_return();
1334-
t->code=new_code;
1335-
t->source_location=new_code.source_location();
1320+
dest.add(goto_programt::make_return(new_code, new_code.source_location()));
13361321
}
13371322
else
13381323
{
@@ -1347,9 +1332,8 @@ void goto_convertt::convert_return(
13471332
unwind_destructor_stack(code.source_location(), 0, dest, mode);
13481333

13491334
// add goto to end-of-function
1350-
goto_programt::targett t=dest.add_instruction();
1351-
t->make_goto(targets.return_target, true_exprt());
1352-
t->source_location=new_code.source_location();
1335+
dest.add(goto_programt::make_goto(
1336+
targets.return_target, new_code.source_location()));
13531337
}
13541338

13551339
void goto_convertt::convert_continue(
@@ -1367,9 +1351,8 @@ void goto_convertt::convert_continue(
13671351
code.source_location(), targets.continue_stack_size, dest, mode);
13681352

13691353
// add goto
1370-
goto_programt::targett t=dest.add_instruction();
1371-
t->make_goto(targets.continue_target);
1372-
t->source_location=code.source_location();
1354+
dest.add(
1355+
goto_programt::make_goto(targets.continue_target, code.source_location()));
13731356
}
13741357

13751358
void goto_convertt::convert_goto(const code_gotot &code, goto_programt &dest)
@@ -1529,11 +1512,8 @@ void goto_convertt::generate_ifthenelse(
15291512
{
15301513
// hmpf. Useless branch.
15311514
goto_programt tmp_z;
1532-
goto_programt::targett z=tmp_z.add_instruction();
1533-
z->make_skip();
1534-
goto_programt::targett v=dest.add_instruction();
1535-
v->make_goto(z, guard);
1536-
v->source_location=source_location;
1515+
goto_programt::targett z = tmp_z.add(goto_programt::make_skip());
1516+
dest.add(goto_programt::make_goto(z, guard, source_location));
15371517
dest.destructive_append(tmp_z);
15381518
return;
15391519
}
@@ -1706,12 +1686,7 @@ void goto_convertt::generate_conditional_branch(
17061686
exprt cond=guard;
17071687
clean_expr(cond, dest, mode);
17081688

1709-
goto_programt tmp;
1710-
goto_programt::targett g=tmp.add_instruction();
1711-
g->make_goto(target_true);
1712-
g->guard=cond;
1713-
g->source_location=source_location;
1714-
dest.destructive_append(tmp);
1689+
dest.add(goto_programt::make_goto(target_true, cond, source_location));
17151690
}
17161691
}
17171692

@@ -1753,10 +1728,7 @@ void goto_convertt::generate_conditional_branch(
17531728
generate_conditional_branch(
17541729
boolean_negate(expr), target_false, source_location, dest, mode);
17551730

1756-
goto_programt::targett t_true=dest.add_instruction();
1757-
t_true->make_goto(target_true);
1758-
t_true->guard=true_exprt();
1759-
t_true->source_location=source_location;
1731+
dest.add(goto_programt::make_goto(target_true, source_location));
17601732

17611733
return;
17621734
}
@@ -1772,30 +1744,25 @@ void goto_convertt::generate_conditional_branch(
17721744
std::list<exprt> op;
17731745
collect_operands(guard, guard.id(), op);
17741746

1747+
// true branch(es)
17751748
for(const auto &expr : op)
17761749
generate_conditional_branch(
17771750
expr, target_true, source_location, dest, mode);
17781751

1779-
goto_programt::targett t_false=dest.add_instruction();
1780-
t_false->make_goto(target_false);
1781-
t_false->guard=true_exprt();
1782-
t_false->source_location=guard.source_location();
1752+
// false branch
1753+
dest.add(goto_programt::make_goto(target_false, guard.source_location()));
17831754

17841755
return;
17851756
}
17861757

17871758
exprt cond=guard;
17881759
clean_expr(cond, dest, mode);
17891760

1790-
goto_programt::targett t_true=dest.add_instruction();
1791-
t_true->make_goto(target_true);
1792-
t_true->guard=cond;
1793-
t_true->source_location=source_location;
1761+
// true branch
1762+
dest.add(goto_programt::make_goto(target_true, cond, source_location));
17941763

1795-
goto_programt::targett t_false=dest.add_instruction();
1796-
t_false->make_goto(target_false);
1797-
t_false->guard=true_exprt();
1798-
t_false->source_location=source_location;
1764+
// false branch
1765+
dest.add(goto_programt::make_goto(target_false, source_location));
17991766
}
18001767

18011768
bool goto_convertt::get_string_constant(
@@ -1994,9 +1961,7 @@ void goto_convertt::generate_thread_block(
19941961
goto_programt::targett a=preamble.add_instruction(START_THREAD);
19951962
a->source_location=thread_body.source_location();
19961963
a->targets.push_back(c);
1997-
goto_programt::targett b=preamble.add_instruction();
1998-
b->source_location=thread_body.source_location();
1999-
b->make_goto(z);
1964+
preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
20001965

20011966
dest.destructive_append(preamble);
20021967
dest.destructive_append(body);

src/goto-programs/goto_program.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -814,6 +814,13 @@ class goto_programt
814814
return instructiont(code_returnt(), irep_idt(), l, RETURN, nil_exprt(), {});
815815
}
816816

817+
static instructiont make_return(
818+
code_returnt c,
819+
const source_locationt &l = source_locationt::nil())
820+
{
821+
return instructiont(std::move(c), irep_idt(), l, RETURN, nil_exprt(), {});
822+
}
823+
817824
static instructiont
818825
make_skip(const source_locationt &l = source_locationt::nil())
819826
{

0 commit comments

Comments
 (0)