Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 13 additions & 15 deletions src/analyses/natural_loops.h
Original file line number Diff line number Diff line change
Expand Up @@ -93,23 +93,21 @@ void natural_loops_templatet<P, T>::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);
}
}
}
Expand Down
8 changes: 2 additions & 6 deletions src/goto-programs/cfg.h
Original file line number Diff line number Diff line change
Expand Up @@ -203,9 +203,7 @@ void cfg_baset<T, P, I>::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<class T, typename P, typename I>
Expand Down Expand Up @@ -260,9 +258,7 @@ void concurrent_cfg_baset<T, P, I>::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<class T, typename P, typename I>
Expand Down
9 changes: 3 additions & 6 deletions src/goto-programs/goto_program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
5 changes: 5 additions & 0 deletions src/goto-programs/goto_program_template.h
Original file line number Diff line number Diff line change
Expand Up @@ -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<irep_idt> labelst;
labelst labels;
Expand Down
5 changes: 1 addition & 4 deletions src/goto-programs/remove_skip.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/symex_start_thread.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down