Merge pull request #1302 from diffblue/goto-get-target

use get_target() where appropriate

Author: kroening

src/analyses/natural_loops.h

@@ -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);
       }
     }
   }

src/goto-programs/cfg.h

@@ -222,9 +222,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>
@@ -279,9 +277,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>

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:

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<irep_idt> labelst;
     labelst labels;

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())

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();