fix half-constructed GOTO instruction

Author: Daniel Kroening

regression/cbmc/goto5/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+void main(void)
+{
+  int r = 0;
+  if ( r == 0 ) 
+  {
+    goto l1;
+    r = 1;
+  }
+  l1:
+  assert(r != 0); // should fail
+}

regression/cbmc/goto5/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

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_convert.cpp

@@ -109,28 +109,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
   {
     goto_programt::instructiont &i=*(g_it.first);
 
-    if(i.code.get_statement()=="non-deterministic-goto")
-    {
-      const irept &destinations=i.code.find("destinations");
-
-      i.make_goto();
-
-      forall_irep(it, destinations.get_sub())
-      {
-        labelst::const_iterator l_it=
-          targets.labels.find(it->id_string());
-
-        if(l_it==targets.labels.end())
-        {
-          error().source_location=i.code.find_source_location();
-          error() << "goto label `" << it->id() << "' not found" << eom;
-          throw 0;
-        }
-
-        i.targets.push_back(l_it->second.first);
-      }
-    }
-    else if(i.is_start_thread())
+    if(i.is_start_thread())
     {
       const irep_idt &goto_label=i.code.get(ID_destination);
 
@@ -159,6 +138,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
         throw 0;
       }
 
+      i.type=GOTO;
       i.targets.clear();
       i.targets.push_back(l_it->second.first);
 
@@ -1480,21 +1460,21 @@ void goto_convertt::convert_goto(
   const codet &code,
   goto_programt &dest)
 {
-  goto_programt::targett t=dest.add_instruction();
-  t->make_goto();
+  // this instruction will turn into a goto during post-processing
+  goto_programt::targett t=dest.add_instruction(NO_INSTRUCTION_TYPE);
   t->source_location=code.source_location();
   t->code=code;
 
-  // remember it to do target later
+  // remember it to do the target later
   targets.gotos.push_back(std::make_pair(t, targets.destructor_stack));
 }
 
 void goto_convertt::convert_gcc_computed_goto(
   const codet &code,
   goto_programt &dest)
 {
-  goto_programt::targett t=dest.add_instruction();
-  t->make_skip();
+  // this instruction will turn into OTHER during post-processing
+  goto_programt::targett t=dest.add_instruction(NO_INSTRUCTION_TYPE);
   t->source_location=code.source_location();
   t->code=code;
 

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