diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index ce27a306882..9eb24ccc0ed 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -93,23 +93,21 @@ void natural_loops_templatet
::compute(P &program)
{
if(m_it->is_backwards_goto())
{
- for(const auto &target : m_it->targets)
+ const auto &target=m_it->get_target();
+
+ if(target->location_number<=m_it->location_number)
{
- if(target->location_number<=m_it->location_number)
- {
- const nodet &node=
- cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
+ const nodet &node=
+ cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]];
-#ifdef DEBUG
- std::cout << "Computing loop for "
- << m_it->location_number << " -> "
- << target->location_number << "\n";
-#endif
- if(node.dominators.find(target)!=node.dominators.end())
- {
- compute_natural_loop(m_it, target);
- }
- }
+ #ifdef DEBUG
+ std::cout << "Computing loop for "
+ << m_it->location_number << " -> "
+ << target->location_number << "\n";
+ #endif
+
+ if(node.dominators.find(target)!=node.dominators.end())
+ compute_natural_loop(m_it, target);
}
}
}
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index 2e1bd83598b..8cd23f8de6d 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -203,9 +203,7 @@ void cfg_baset::compute_edges_goto(
!instruction.guard.is_true())
this->add_edge(entry, entry_map[next_PC]);
- for(const auto &t : instruction.targets)
- if(t!=goto_program.instructions.end())
- this->add_edge(entry, entry_map[t]);
+ this->add_edge(entry, entry_map[instruction.get_target()]);
}
template
@@ -260,9 +258,7 @@ void concurrent_cfg_baset::compute_edges_start_thread(
next_PC,
entry);
- for(const auto &t : instruction.targets)
- if(t!=goto_program.instructions.end())
- this->add_edge(entry, this->entry_map[t]);
+ this->add_edge(entry, this->entry_map[instruction.get_target()]);
}
template
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 44546821019..6cf8414899a 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -212,12 +212,9 @@ std::ostream &goto_programt::output_instruction(
break;
case START_THREAD:
- out << "START THREAD ";
-
- if(instruction.targets.size()==1)
- out << instruction.targets.front()->target_number;
-
- out << '\n';
+ out << "START THREAD "
+ << instruction.get_target()->target_number
+ << '\n';
break;
case END_THREAD:
diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h
index 986888e4ca3..aa863a5dd0f 100644
--- a/src/goto-programs/goto_program_template.h
+++ b/src/goto-programs/goto_program_template.h
@@ -199,6 +199,11 @@ class goto_program_templatet
targets.push_back(t);
}
+ bool has_target() const
+ {
+ return !targets.empty();
+ }
+
/// Goto target labels
typedef std::list labelst;
labelst labels;
diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp
index 3529a8f2018..231ed117f31 100644
--- a/src/goto-programs/remove_skip.cpp
+++ b/src/goto-programs/remove_skip.cpp
@@ -28,16 +28,13 @@ static bool is_skip(goto_programt::instructionst::iterator it)
if(it->guard.is_false())
return true;
- if(it->targets.size()!=1)
- return false;
-
goto_programt::instructionst::iterator next_it=it;
next_it++;
// A branch to the next instruction is a skip
// We also require the guard to be 'true'
return it->guard.is_true() &&
- it->targets.front()==next_it;
+ it->get_target()==next_it;
}
if(it->is_other())
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 8ebed5216c1..db276719654 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -32,7 +32,7 @@ void goto_symext::symex_start_thread(statet &state)
throw "start_thread expects one target";
goto_programt::const_targett thread_target=
- instruction.targets.front();
+ instruction.get_target();
// put into thread vector
std::size_t t=state.threads.size();