Skip to content

Commit c2c9f1b

Browse files
author
Daniel Kroening
committed
use get_target() where appropriate
1 parent df16159 commit c2c9f1b

File tree

6 files changed

+25
-32
lines changed

6 files changed

+25
-32
lines changed

src/analyses/natural_loops.h

Lines changed: 13 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -93,23 +93,21 @@ void natural_loops_templatet<P, T>::compute(P &program)
9393
{
9494
if(m_it->is_backwards_goto())
9595
{
96-
for(const auto &target : m_it->targets)
96+
const auto &target=m_it->get_target();
97+
98+
if(target->location_number<=m_it->location_number)
9799
{
98-
if(target->location_number<=m_it->location_number)
99-
{
100-
const nodet &node=
101-
cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
100+
const nodet &node=
101+
cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
102102

103-
#ifdef DEBUG
104-
std::cout << "Computing loop for "
105-
<< m_it->location_number << " -> "
106-
<< target->location_number << "\n";
107-
#endif
108-
if(node.dominators.find(target)!=node.dominators.end())
109-
{
110-
compute_natural_loop(m_it, target);
111-
}
112-
}
103+
#ifdef DEBUG
104+
std::cout << "Computing loop for "
105+
<< m_it->location_number << " -> "
106+
<< target->location_number << "\n";
107+
#endif
108+
109+
if(node.dominators.find(target)!=node.dominators.end())
110+
compute_natural_loop(m_it, target);
113111
}
114112
}
115113
}

src/goto-programs/cfg.h

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -203,9 +203,7 @@ void cfg_baset<T, P, I>::compute_edges_goto(
203203
!instruction.guard.is_true())
204204
this->add_edge(entry, entry_map[next_PC]);
205205

206-
for(const auto &t : instruction.targets)
207-
if(t!=goto_program.instructions.end())
208-
this->add_edge(entry, entry_map[t]);
206+
this->add_edge(entry, entry_map[instruction.get_target()]);
209207
}
210208

211209
template<class T, typename P, typename I>
@@ -260,9 +258,7 @@ void concurrent_cfg_baset<T, P, I>::compute_edges_start_thread(
260258
next_PC,
261259
entry);
262260

263-
for(const auto &t : instruction.targets)
264-
if(t!=goto_program.instructions.end())
265-
this->add_edge(entry, this->entry_map[t]);
261+
this->add_edge(entry, this->entry_map[instruction.get_target()]);
266262
}
267263

268264
template<class T, typename P, typename I>

src/goto-programs/goto_program.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -212,12 +212,9 @@ std::ostream &goto_programt::output_instruction(
212212
break;
213213

214214
case START_THREAD:
215-
out << "START THREAD ";
216-
217-
if(instruction.targets.size()==1)
218-
out << instruction.targets.front()->target_number;
219-
220-
out << '\n';
215+
out << "START THREAD "
216+
<< instruction.get_target()->target_number
217+
<< '\n';
221218
break;
222219

223220
case END_THREAD:

src/goto-programs/goto_program_template.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -199,6 +199,11 @@ class goto_program_templatet
199199
targets.push_back(t);
200200
}
201201

202+
bool has_target() const
203+
{
204+
return !targets.empty();
205+
}
206+
202207
/// Goto target labels
203208
typedef std::list<irep_idt> labelst;
204209
labelst labels;

src/goto-programs/remove_skip.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,16 +28,13 @@ static bool is_skip(goto_programt::instructionst::iterator it)
2828
if(it->guard.is_false())
2929
return true;
3030

31-
if(it->targets.size()!=1)
32-
return false;
33-
3431
goto_programt::instructionst::iterator next_it=it;
3532
next_it++;
3633

3734
// A branch to the next instruction is a skip
3835
// We also require the guard to be 'true'
3936
return it->guard.is_true() &&
40-
it->targets.front()==next_it;
37+
it->get_target()==next_it;
4138
}
4239

4340
if(it->is_other())

src/goto-symex/symex_start_thread.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ void goto_symext::symex_start_thread(statet &state)
3232
throw "start_thread expects one target";
3333

3434
goto_programt::const_targett thread_target=
35-
instruction.targets.front();
35+
instruction.get_target();
3636

3737
// put into thread vector
3838
std::size_t t=state.threads.size();

0 commit comments

Comments
 (0)