Avoid the use of is_backwards_goto while unwinding

The method may in some cases (e.g. ite4 termination regression test)
cause a segfault for unknown reasons. Flip the condition, check using
incoming edges if an instruction is loop head rather than checking
if a goto is loop exit.

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

src/2ls/preprocessing_util.cpp

@@ -114,13 +114,22 @@ bool twols_parse_optionst::unwind_goto_into_loop(
     loopst loops;
     Forall_goto_program_instructions(i_it, body)
     {
-      if(i_it->is_backwards_goto())
+      bool is_loop_head=false;
+      goto_programt::targett loop_exit;
+      for(auto edge : i_it->incoming_edges)
+      {
+        if(edge->location_number>i_it->location_number)
+        {
+          is_loop_head=true;
+          loop_exit=edge;
+        }
+      }
+
+      if(is_loop_head)
       {
-        goto_programt::targett loop_head=i_it->get_target();
-        goto_programt::targett loop_exit=i_it;
         bool has_goto_into_loop=false;
 
-        goto_programt::targett it=loop_head;
+        goto_programt::targett it=i_it;
         if(it!=loop_exit)
           it++;
         for(; it!=loop_exit; it++)
@@ -130,7 +139,7 @@ bool twols_parse_optionst::unwind_goto_into_loop(
                s_it!=it->incoming_edges.end(); ++s_it)
           {
             if((*s_it)->is_goto() &&
-               (*s_it)->location_number<loop_head->location_number)
+               (*s_it)->location_number<i_it->location_number)
             {
               has_goto_into_loop=true;
               result=true;
@@ -143,7 +152,7 @@ bool twols_parse_optionst::unwind_goto_into_loop(
         if(has_goto_into_loop)
         {
           status() << "Unwinding jump into loop" << eom;
-          loops.push_back(loopst::value_type(++loop_exit, loop_head));
+          loops.push_back(loopst::value_type(++loop_exit, i_it));
         }
       }
     }