prevent half-constructed GOTO instructions

Author: Daniel Kroening

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -306,9 +306,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
   // Jump to the universal handler or function end, as appropriate.
   // This will appear after the GOTO-based dynamic dispatch below
   goto_programt::targett default_dispatch=goto_program.insert_after(instr_it);
-  default_dispatch->make_goto();
-  default_dispatch->source_location=instr_it->source_location;
-  default_dispatch->function=instr_it->function;
 
   // find the symbol corresponding to the caught exceptions
   symbol_exprt exc_thrown =
@@ -356,7 +353,9 @@ void remove_exceptionst::add_exception_dispatch_sequence(
     }
   }
 
-  default_dispatch->set_target(default_target);
+  default_dispatch->make_goto(default_target);
+  default_dispatch->source_location=instr_it->source_location;
+  default_dispatch->function=instr_it->function;
 
   // add dead instructions
   for(const auto &local : locals)

src/goto-instrument/accelerate/accelerate.cpp

@@ -212,16 +212,12 @@ void acceleratet::insert_looping_path(
   ++loop_body;
 
   goto_programt::targett jump=program.insert_before(loop_body);
-  jump->make_goto();
-  jump->guard=side_effect_expr_nondett(bool_typet());
-  jump->targets.push_back(loop_body);
+  jump->make_goto(loop_body, side_effect_expr_nondett(bool_typet()));
 
   program.destructive_insert(loop_body, looping_path);
 
   jump=program.insert_before(loop_body);
-  jump->make_goto();
-  jump->guard=true_exprt();
-  jump->targets.push_back(back_jump);
+  jump->make_goto(back_jump, true_exprt());
 
   for(goto_programt::targett t=loop_header;
       t!=loop_body;

src/goto-instrument/branch.cpp

@@ -56,8 +56,7 @@ void branch(
         t1->function=f_it->first;
 
         goto_programt::targett t2=body.insert_after(t1);
-        t2->make_goto();
-        t2->targets=i_it->targets;
+        t2->make_goto(i_it->get_target());
 
         goto_programt::targett t3=body.insert_after(t2);
         t3->make_function_call(

src/goto-programs/goto_program.h

@@ -237,7 +237,6 @@ class goto_programt
       code.make_nil();
     }
 
-    void make_goto() { clear(GOTO); }
     void make_return() { clear(RETURN); }
     void make_skip() { clear(SKIP); }
     void make_location(const source_locationt &l)
@@ -256,7 +255,7 @@ class goto_programt
 
     void make_goto(targett _target)
     {
-      make_goto();
+      clear(GOTO);
       targets.push_back(_target);
     }