avoid goto_programt::insert_before and _after without instruction

Instead use the variant that takes the instruction to be constructed as
parameter, thereby avoiding duplicate assignment.

Author: Daniel Kroening

src/goto-instrument/accelerate/accelerate.cpp

@@ -258,24 +258,19 @@ void acceleratet::make_overflow_loc(
     loop.insert(added.begin(), added.end());
   }
 
-  goto_programt::targett t=program.insert_after(loop_header);
-  *t =
-    goto_programt::make_assignment(code_assignt(overflow_var, false_exprt()));
+  goto_programt::targett t = program.insert_after(
+    loop_header,
+    goto_programt::make_assignment(code_assignt(overflow_var, false_exprt())));
   t->swap(*loop_header);
   loop.insert(t);
   overflow_locs[loop_header].push_back(t);
 
-  goto_programt::instructiont s(SKIP);
-  overflow_loc=program.insert_after(loop_end);
-  *overflow_loc=s;
+  overflow_loc = program.insert_after(loop_end, goto_programt::make_skip());
   overflow_loc->swap(*loop_end);
   loop.insert(overflow_loc);
 
-  goto_programt::instructiont g =
-    goto_programt::make_goto(overflow_loc, not_exprt(overflow_var));
-
-  goto_programt::targett t2=program.insert_after(loop_end);
-  *t2=g;
+  goto_programt::targett t2 = program.insert_after(
+    loop_end, goto_programt::make_goto(overflow_loc, not_exprt(overflow_var)));
   t2->swap(*loop_end);
   overflow_locs[overflow_loc].push_back(t2);
   loop.insert(t2);

src/goto-instrument/accelerate/overflow_instrumenter.cpp

@@ -286,10 +286,9 @@ void overflow_instrumentert::accumulate_overflow(
   const exprt &expr,
   goto_programt::targetst &added)
 {
-  goto_programt::instructiont a(ASSIGN);
-  a.code=code_assignt(overflow_var, or_exprt(overflow_var, expr));
-  goto_programt::targett assignment=program.insert_after(t);
-  *assignment=a;
+  goto_programt::targett assignment = program.insert_after(
+    t,
+    goto_programt::make_assignment(overflow_var, or_exprt(overflow_var, expr)));
   assignment->swap(*t);
 
   added.push_back(assignment);

src/goto-instrument/race_check.cpp

@@ -99,9 +99,8 @@ void w_guardst::add_initialization(goto_programt &goto_program) const
   {
     exprt symbol=ns.lookup(*it).symbol_expr();
 
-    t=goto_program.insert_before(t);
-    t->type=ASSIGN;
-    t->code=code_assignt(symbol, false_exprt());
+    t = goto_program.insert_before(
+      t, goto_programt::make_assignment(symbol, false_exprt()));
 
     t++;
   }
@@ -199,14 +198,12 @@ static void race_check(
         if(!is_shared(ns, e_it->second.symbol_expr))
           continue;
 
-        goto_programt::targett t=goto_program.insert_before(i_it);
-
-        t->type=ASSIGN;
-        t->code=code_assignt(
-          w_guards.get_w_guard_expr(e_it->second),
-          e_it->second.guard);
-
-        t->source_location=original_instruction.source_location;
+        goto_programt::targett t = goto_program.insert_before(
+          i_it,
+          goto_programt::make_assignment(
+            w_guards.get_w_guard_expr(e_it->second),
+            e_it->second.guard,
+            original_instruction.source_location));
         i_it=++t;
       }
 
@@ -223,15 +220,13 @@ static void race_check(
         if(!is_shared(ns, e_it->second.symbol_expr))
           continue;
 
-        goto_programt::targett t=goto_program.insert_before(i_it);
-
-        t->type=ASSIGN;
-        t->code=code_assignt(
-          w_guards.get_w_guard_expr(e_it->second),
-          false_exprt());
-
-        t->source_location=original_instruction.source_location;
-        i_it=++t;
+        goto_programt::targett t = goto_program.insert_before(
+          i_it,
+          goto_programt::make_assignment(
+            w_guards.get_w_guard_expr(e_it->second),
+            false_exprt(),
+            original_instruction.source_location));
+        i_it = std::next(t);
       }
 
       // now add assertions for what is read and written

src/goto-programs/goto_convert.cpp

@@ -216,11 +216,9 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
 
       const equal_exprt guard(pointer, address_of_exprt(label_expr));
 
-      goto_programt::targett t=
-        goto_program.insert_after(g_it);
-
-      *t =
-        goto_programt::make_goto(label.second.first, guard, i.source_location);
+      goto_program.insert_after(
+        g_it,
+        goto_programt::make_goto(label.second.first, guard, i.source_location));
     }
   }