From 1f6762fef171faca1ef10e3d61ba1e2a5e50f1a5 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 13 Feb 2019 15:55:20 +0000
Subject: [PATCH 1/5] use instructiont::turn_into_skip

This is a clearer idiom.
---
 jbmc/src/java_bytecode/remove_instanceof.cpp                    | 2 +-
 .../accelerate/disjunctive_polynomial_acceleration.cpp          | 2 +-
 src/goto-instrument/accelerate/sat_path_enumerator.cpp          | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp
index 772cdeb18d8..02a4c733b8b 100644
--- a/jbmc/src/java_bytecode/remove_instanceof.cpp
+++ b/jbmc/src/java_bytecode/remove_instanceof.cpp
@@ -211,7 +211,7 @@ bool remove_instanceoft::lower_instanceof(
     // GOTO programs before the target instruction without inserting into the
     // wrong basic block.
     goto_program.insert_before_swap(target);
-    *target = goto_programt::make_skip();
+    target->turn_into_skip();
     // Actually alter the now-moved instruction:
     ++target;
   }
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index 91e45ecc86a..de17d162fce 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -914,7 +914,7 @@ void disjunctive_polynomial_accelerationt::build_fixed()
     if(loop.find(t)==loop.end())
     {
       // This instruction isn't part of the loop...  Just remove it.
-      *fixedt = goto_programt::make_skip(fixedt->source_location);
+      fixedt->turn_into_skip();
       continue;
     }
 
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index 2b1ba041fd0..84fbff62239 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -269,7 +269,7 @@ void sat_path_enumeratort::build_fixed()
     if(loop.find(t)==loop.end())
     {
       // This instruction isn't part of the loop...  Just remove it.
-      *fixedt = goto_programt::make_skip(fixedt->source_location);
+      fixedt->turn_into_skip();
       continue;
     }
 

From c6dba6a1b100d35e8c9c38bec9021b0976f99f35 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 13 Feb 2019 16:02:01 +0000
Subject: [PATCH 2/5] prefer .add over .emplace

This is easier to read.
---
 unit/goto-programs/goto_program_assume.cpp      | 7 +++----
 unit/goto-programs/goto_program_declaration.cpp | 3 +--
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp
index dc0f1db2d5d..710b03ada46 100644
--- a/unit/goto-programs/goto_program_assume.cpp
+++ b/unit/goto-programs/goto_program_assume.cpp
@@ -31,14 +31,13 @@ SCENARIO(
     binary_relation_exprt x_le_10(varx, ID_le, val10);
 
     goto_functiont goto_function;
-    auto &instructions = goto_function.body.instructions;
-    instructions.emplace_back(goto_program_instruction_typet::ASSUME);
+    auto assertion =
+      goto_function.body.add(goto_programt::make_assertion(x_le_10));
 
     symbol.type = type1;
     symbol_table.insert(symbol);
     symbol_table.insert(fun_symbol);
     namespacet ns(symbol_table);
-    instructions.back() = goto_programt::make_assertion(x_le_10);
 
     WHEN("Instruction has no targets")
     {
@@ -51,7 +50,7 @@ SCENARIO(
 
     WHEN("Instruction has a target")
     {
-      instructions.back().targets.push_back(instructions.begin());
+      assertion->targets.push_back(assertion);
       THEN("The consistency check fails")
       {
         REQUIRE_THROWS_AS(
diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp
index 19fed687358..95203c6b498 100644
--- a/unit/goto-programs/goto_program_declaration.cpp
+++ b/unit/goto-programs/goto_program_declaration.cpp
@@ -32,8 +32,7 @@ SCENARIO(
     symbol_exprt var_a(var_symbol_name, type1);
 
     goto_functiont goto_function;
-    auto &instructions = goto_function.body.instructions;
-    instructions.emplace_back(goto_programt::make_decl(var_a));
+    goto_function.body.add(goto_programt::make_decl(var_a));
     symbol_table.insert(fun_symbol);
 
     WHEN("Declaring known symbol")

From 9e596c939fd8c9afd9472095c3138e77d5f869b1 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 13 Feb 2019 16:04:56 +0000
Subject: [PATCH 3/5] use make_assignment(lhs, rhs)

This is slightly shorter.
---
 src/analyses/goto_check.cpp                  |  5 +-
 src/goto-instrument/dump_c.cpp               |  2 +-
 src/goto-programs/string_abstraction.cpp     | 27 +++++------
 src/goto-programs/string_instrumentation.cpp | 51 +++++++-------------
 4 files changed, 33 insertions(+), 52 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 3177cfa791e..5ca8300808b 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1852,7 +1852,7 @@ void goto_checkt::goto_check(
             lhs);
           goto_programt::targett t =
             new_code.add(goto_programt::make_assignment(
-              code_assignt(std::move(lhs), std::move(rhs)), i.source_location));
+              std::move(lhs), std::move(rhs), i.source_location));
           t->code.add_source_location()=i.source_location;
         }
       }
@@ -1867,8 +1867,7 @@ void goto_checkt::goto_check(
         const symbol_exprt leak_expr=leak.symbol_expr();
 
         // add self-assignment to get helpful counterexample output
-        new_code.add(
-          goto_programt::make_assignment(code_assignt(leak_expr, leak_expr)));
+        new_code.add(goto_programt::make_assignment(leak_expr, leak_expr));
 
         source_locationt source_location;
         source_location.set_function(function_identifier);
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 9c331dcb86d..77aa0c4d2e9 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -593,7 +593,7 @@ void dump_ct::cleanup_decl(
   tmp.add(goto_programt::make_decl(decl.symbol()));
 
   if(value.is_not_nil())
-    tmp.add(goto_programt::make_assignment(code_assignt(decl.op0(), value)));
+    tmp.add(goto_programt::make_assignment(decl.symbol(), value));
 
   tmp.add(goto_programt::make_end_function());
 
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 0e27fadf7b9..0508a002687 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -1281,30 +1281,27 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct(
   goto_programt tmp;
 
   {
-    goto_programt::targett assignment=tmp.add_instruction(ASSIGN);
-    assignment->code=code_assignt(
-        member(lhs, whatt::IS_ZERO),
-        member(rhs, whatt::IS_ZERO));
+    goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
+      member(lhs, whatt::IS_ZERO),
+      member(rhs, whatt::IS_ZERO),
+      target->source_location));
     assignment->code.add_source_location()=target->source_location;
-    assignment->source_location=target->source_location;
   }
 
   {
-    goto_programt::targett assignment=tmp.add_instruction(ASSIGN);
-    assignment->code=code_assignt(
-        member(lhs, whatt::LENGTH),
-        member(rhs, whatt::LENGTH));
+    goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
+      member(lhs, whatt::LENGTH),
+      member(rhs, whatt::LENGTH),
+      target->source_location));
     assignment->code.add_source_location()=target->source_location;
-    assignment->source_location=target->source_location;
   }
 
   {
-    goto_programt::targett assignment=tmp.add_instruction(ASSIGN);
-    assignment->code=code_assignt(
-        member(lhs, whatt::SIZE),
-        member(rhs, whatt::SIZE));
+    goto_programt::targett assignment = tmp.add(goto_programt::make_assignment(
+      member(lhs, whatt::SIZE),
+      member(rhs, whatt::SIZE),
+      target->source_location));
     assignment->code.add_source_location()=target->source_location;
-    assignment->source_location=target->source_location;
   }
 
   goto_programt::targett last=target;
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
index d88d136fb16..a502df8dbac 100644
--- a/src/goto-programs/string_instrumentation.cpp
+++ b/src/goto-programs/string_instrumentation.cpp
@@ -296,13 +296,11 @@ void string_instrumentationt::do_sprintf(
 
   if(call.lhs().is_not_nil())
   {
-    goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
-    return_assignment->source_location=target->source_location;
-
     exprt rhs =
       side_effect_expr_nondett(call.lhs().type(), target->source_location);
 
-    return_assignment->code=code_assignt(call.lhs(), rhs);
+    tmp.add(
+      goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
   }
 
   target->turn_into_skip();
@@ -337,13 +335,11 @@ void string_instrumentationt::do_snprintf(
 
   if(call.lhs().is_not_nil())
   {
-    goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
-    return_assignment->source_location=target->source_location;
-
     exprt rhs =
       side_effect_expr_nondett(call.lhs().type(), target->source_location);
 
-    return_assignment->code=code_assignt(call.lhs(), rhs);
+    tmp.add(
+      goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
   }
 
   target->turn_into_skip();
@@ -369,13 +365,11 @@ void string_instrumentationt::do_fscanf(
 
   if(call.lhs().is_not_nil())
   {
-    goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
-    return_assignment->source_location=target->source_location;
-
     exprt rhs =
       side_effect_expr_nondett(call.lhs().type(), target->source_location);
 
-    return_assignment->code=code_assignt(call.lhs(), rhs);
+    tmp.add(
+      goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
   }
 
   target->turn_into_skip();
@@ -560,14 +554,12 @@ void string_instrumentationt::do_format_string_write(
           const exprt &argument=arguments[argument_start_inx+args];
           const typet &arg_type = argument.type();
 
-          goto_programt::targett assignment=dest.add_instruction(ASSIGN);
-          assignment->source_location=target->source_location;
-
           const dereference_exprt lhs(argument, arg_type.subtype());
 
           side_effect_expr_nondett rhs(lhs.type(), target->source_location);
 
-          assignment->code=code_assignt(lhs, rhs);
+          dest.add(
+            goto_programt::make_assignment(lhs, rhs, target->source_location));
 
           args++;
           break;
@@ -602,14 +594,12 @@ void string_instrumentationt::do_format_string_write(
       }
       else
       {
-        goto_programt::targett assignment=dest.add_instruction(ASSIGN);
-        assignment->source_location=target->source_location;
-
         dereference_exprt lhs(arguments[i], arg_type.subtype());
 
         side_effect_expr_nondett rhs(lhs.type(), target->source_location);
 
-        assignment->code=code_assignt(lhs, rhs);
+        dest.add(
+          goto_programt::make_assignment(lhs, rhs, target->source_location));
       }
     }
   }
@@ -804,11 +794,8 @@ void string_instrumentationt::do_strerror(
   address_of_exprt ptr(index);
 
   // make that zero-terminated
-  {
-    goto_programt::targett assignment2=tmp.add_instruction(ASSIGN);
-    assignment2->code=code_assignt(is_zero_string(ptr, true), true_exprt());
-    assignment2->source_location=it->source_location;
-  }
+  tmp.add(goto_programt::make_assignment(
+    is_zero_string(ptr, true), true_exprt(), it->source_location));
 
   // assign address
   {
@@ -851,23 +838,21 @@ void string_instrumentationt::invalidate_buffer(
   // create a loop that runs over the buffer
   // and invalidates every element
 
-  goto_programt::targett init=dest.add_instruction(ASSIGN);
-  init->source_location=target->source_location;
-  init->code=
-    code_assignt(cntr_sym.symbol_expr(), from_integer(0, cntr_sym.type));
+  dest.add(goto_programt::make_assignment(
+    cntr_sym.symbol_expr(),
+    from_integer(0, cntr_sym.type),
+    target->source_location));
 
   goto_programt::targett check=dest.add_instruction();
 
   goto_programt::targett invalidate=dest.add_instruction(ASSIGN);
   invalidate->source_location=target->source_location;
 
-  goto_programt::targett increment=dest.add_instruction(ASSIGN);
-  increment->source_location=target->source_location;
-
   const plus_exprt plus(
     cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
 
-  increment->code=code_assignt(cntr_sym.symbol_expr(), plus);
+  dest.add(goto_programt::make_assignment(
+    cntr_sym.symbol_expr(), plus, target->source_location));
 
   dest.add(
     goto_programt::make_goto(check, true_exprt(), target->source_location));

From 82d7ce9343af383c09b05a07e9ec3cc2d64ff68d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 13 Feb 2019 16:09:26 +0000
Subject: [PATCH 4/5] avoid access to instructiont::code

This will allow protecting instructiont::code.
---
 src/analyses/constant_propagator.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index d361272f09f..9be0cdf1b51 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -156,13 +156,13 @@ void constant_propagator_domaint::transform(
 
   if(from->is_decl())
   {
-    const code_declt &code_decl=to_code_decl(from->code);
+    const auto &code_decl = from->get_decl();
     const symbol_exprt &symbol = code_decl.symbol();
     values.set_to_top(symbol);
   }
   else if(from->is_assign())
   {
-    const code_assignt &assignment=to_code_assign(from->code);
+    const auto &assignment = from->get_assign();
     const exprt &lhs=assignment.lhs();
     const exprt &rhs=assignment.rhs();
     assign_rec(values, lhs, rhs, ns, cp, true);
@@ -189,12 +189,12 @@ void constant_propagator_domaint::transform(
   }
   else if(from->is_dead())
   {
-    const code_deadt &code_dead=to_code_dead(from->code);
+    const auto &code_dead = from->get_dead();
     values.set_to_top(code_dead.symbol());
   }
   else if(from->is_function_call())
   {
-    const code_function_callt &function_call=to_code_function_call(from->code);
+    const auto &function_call = from->get_function_call();
     const exprt &function=function_call.function();
 
     if(function.id()==ID_symbol)

From cba52e3a399347b045e8badb04d531296ef7d504 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 16 Feb 2019 10:26:57 +0000
Subject: [PATCH 5/5] use goto_programt::make_X

This avoids incomplete construction.
---
 src/assembler/remove_asm.cpp                  |  12 +-
 src/goto-analyzer/taint_analysis.cpp          |   2 +-
 .../accelerate/polynomial_accelerator.cpp     |  26 ++--
 .../accelerate/sat_path_enumerator.cpp        |   8 +-
 src/goto-programs/builtin_functions.cpp       | 130 +++++++-----------
 src/goto-programs/goto_convert.cpp            |  16 +--
 src/goto-programs/goto_convert_exceptions.cpp |  13 +-
 .../goto_convert_function_call.cpp            |  11 +-
 src/goto-programs/goto_inline_class.cpp       |   4 +-
 src/goto-programs/remove_calls_no_body.cpp    |   4 +-
 10 files changed, 87 insertions(+), 139 deletions(-)

diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
index 7c37687fe79..44fc39c577f 100644
--- a/src/assembler/remove_asm.cpp
+++ b/src/assembler/remove_asm.cpp
@@ -266,8 +266,7 @@ void remove_asmt::process_instruction_gcc(
 
     if(x86_32_locked_atomic)
     {
-      goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN);
-      ab->source_location = code.source_location();
+      tmp_dest.add(goto_programt::make_atomic_begin(code.source_location()));
 
       codet code_fence(ID_fence);
       code_fence.add_source_location() = code.source_location();
@@ -360,8 +359,7 @@ void remove_asmt::process_instruction_gcc(
 
     if(x86_32_locked_atomic)
     {
-      goto_programt::targett ae = tmp_dest.add_instruction(ATOMIC_END);
-      ae->source_location = code.source_location();
+      tmp_dest.add(goto_programt::make_atomic_end(code.source_location()));
 
       x86_32_locked_atomic = false;
     }
@@ -437,8 +435,7 @@ void remove_asmt::process_instruction_msc(
 
     if(x86_32_locked_atomic)
     {
-      goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN);
-      ab->source_location = code.source_location();
+      tmp_dest.add(goto_programt::make_atomic_begin(code.source_location()));
 
       codet code_fence(ID_fence);
       code_fence.add_source_location() = code.source_location();
@@ -465,8 +462,7 @@ void remove_asmt::process_instruction_msc(
 
     if(x86_32_locked_atomic)
     {
-      goto_programt::targett ae = tmp_dest.add_instruction(ATOMIC_END);
-      ae->source_location = code.source_location();
+      tmp_dest.add(goto_programt::make_atomic_end(code.source_location()));
 
       x86_32_locked_atomic = false;
     }
diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
index d4fa0ea3929..77da60bb3cc 100644
--- a/src/goto-analyzer/taint_analysis.cpp
+++ b/src/goto-analyzer/taint_analysis.cpp
@@ -276,7 +276,7 @@ bool taint_analysist::operator()(
 
       goto_programt end, gotos, calls;
 
-      end.add_instruction(END_FUNCTION);
+      end.add(goto_programt::make_end_function());
 
       forall_goto_functions(f_it, goto_functions)
         if(f_it->second.body_available() &&
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 28dc7f720bf..746596aa469 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -235,7 +235,7 @@ bool polynomial_acceleratort::accelerate(
   // assume(guard);
   // assume(no overflows in previous code);
 
-  program.add_instruction(ASSUME)->guard=guard;
+  program.add(goto_programt::make_assumption(guard));
 
   program.assign(
     loop_counter,
@@ -261,7 +261,7 @@ bool polynomial_acceleratort::accelerate(
     return false;
   }
 
-  program.add_instruction(ASSUME)->guard=guard_last;
+  program.add(goto_programt::make_assumption(guard_last));
   program.fix_types();
 
   if(path_is_monotone)
@@ -406,9 +406,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
 #endif
 
   // Now do an ASSERT(false) to grab a counterexample
-  goto_programt::targett assertion=program.add_instruction(ASSERT);
-  assertion->guard=false_exprt();
-
+  program.add(goto_programt::make_assertion(false_exprt()));
 
   // If the path is satisfiable, we've fitted a polynomial.  Extract the
   // relevant coefficients and return the expression.
@@ -600,7 +598,7 @@ void polynomial_acceleratort::assert_for_values(
   exprt overflow_expr;
   overflow.overflow_expr(rhs, overflow_expr);
 
-  program.add_instruction(ASSUME)->guard=not_exprt(overflow_expr);
+  program.add(goto_programt::make_assumption(not_exprt(overflow_expr)));
 
   rhs=typecast_exprt(rhs, target.type());
 
@@ -609,8 +607,7 @@ void polynomial_acceleratort::assert_for_values(
   const equal_exprt polynomial_holds(target, rhs);
 
   // Finally, assert that the polynomial equals the variable we're fitting.
-  goto_programt::targett assumption=program.add_instruction(ASSUME);
-  assumption->guard=polynomial_holds;
+  program.add(goto_programt::make_assumption(polynomial_holds));
 }
 
 void polynomial_acceleratort::cone_of_influence(
@@ -680,24 +677,23 @@ bool polynomial_acceleratort::check_inductive(
       ++it)
   {
     const equal_exprt holds(it->first, it->second.to_expr());
-    program.add_instruction(ASSUME)->guard=holds;
+    program.add(goto_programt::make_assumption(holds));
 
     polynomials_hold.push_back(holds);
   }
 
   program.append(body);
 
-  codet inc_loop_counter=
-    code_assignt(
-      loop_counter,
-      plus_exprt(loop_counter, from_integer(1, loop_counter.type())));
-  program.add_instruction(ASSIGN)->code=inc_loop_counter;
+  auto inc_loop_counter = code_assignt(
+    loop_counter,
+    plus_exprt(loop_counter, from_integer(1, loop_counter.type())));
+  program.add(goto_programt::make_assignment(inc_loop_counter));
 
   for(std::vector<exprt>::iterator it=polynomials_hold.begin();
       it!=polynomials_hold.end();
       ++it)
   {
-    program.add_instruction(ASSERT)->guard=*it;
+    program.add(goto_programt::make_assertion(*it));
   }
 
 #ifdef DEBUG
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index 84fbff62239..3dd2bb2ab36 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -79,7 +79,7 @@ bool sat_path_enumeratort::next(patht &path)
     program.assume(new_path);
   }
 
-  program.add_instruction(ASSERT)->guard=false_exprt();
+  program.add(goto_programt::make_assertion(false_exprt()));
 
   try
   {
@@ -227,13 +227,13 @@ void sat_path_enumeratort::build_fixed()
   // As such, any path that jumps outside of the loop or jumps backwards
   // to a location other than the loop header (i.e. a nested loop) is not
   // one we're interested in, and we'll redirect it to this assume(false).
-  goto_programt::targett kill=fixed.add_instruction(ASSUME);
-  kill->guard=false_exprt();
+  goto_programt::targett kill =
+    fixed.add(goto_programt::make_assumption(false_exprt()));
 
   // Make a sentinel instruction to mark the end of the loop body.
   // We'll use this as the new target for any back-jumps to the loop
   // header.
-  goto_programt::targett end=fixed.add_instruction(SKIP);
+  goto_programt::targett end = fixed.add(goto_programt::make_skip());
 
   // A pointer to the start of the fixed-path body.  We'll be using this to
   // iterate over the fixed-path body, but for now it's just a pointer to the
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 0792f2e086e..0ae447cb310 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -392,8 +392,7 @@ void goto_convertt::do_atomic_begin(
     throw 0;
   }
 
-  goto_programt::targett t=dest.add_instruction(ATOMIC_BEGIN);
-  t->source_location=function.source_location();
+  dest.add(goto_programt::make_atomic_begin(function.source_location()));
 }
 
 void goto_convertt::do_atomic_end(
@@ -416,8 +415,7 @@ void goto_convertt::do_atomic_end(
     throw 0;
   }
 
-  goto_programt::targett t=dest.add_instruction(ATOMIC_END);
-  t->source_location=function.source_location();
+  dest.add(goto_programt::make_atomic_end(function.source_location()));
 }
 
 void goto_convertt::do_cpp_new(
@@ -526,10 +524,10 @@ void goto_convertt::do_cpp_new(
     throw 0;
   }
 
-  goto_programt::targett t_n=dest.add_instruction(ASSIGN);
-  t_n->code=code_assignt(
-    lhs, typecast_exprt(tmp_symbol_expr, lhs.type()));
-  t_n->source_location=rhs.find_source_location();
+  dest.add(goto_programt::make_assignment(
+    lhs,
+    typecast_exprt(tmp_symbol_expr, lhs.type()),
+    rhs.find_source_location()));
 
   // grab initializer
   goto_programt tmp_initializer;
@@ -815,11 +813,11 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    goto_programt::targett t=dest.add_instruction(OTHER);
-    t->source_location=function.source_location();
-    t->code=codet(ID_havoc_object);
-    t->code.add_source_location()=function.source_location();
-    t->code.copy_to_operands(arguments[0]);
+    codet havoc(ID_havoc_object);
+    havoc.add_source_location() = function.source_location();
+    havoc.copy_to_operands(arguments[0]);
+
+    dest.add(goto_programt::make_other(havoc, function.source_location()));
   }
   else if(identifier==CPROVER_PREFIX "printf")
   {
@@ -1066,11 +1064,9 @@ void goto_convertt::do_function_call_symbol(
     }
 
     codet fence(ID_fence);
+
     forall_expr(it, arguments)
-    {
-      const irep_idt kind=get_string_constant(*it);
-      fence.set(kind, true);
-    }
+      fence.set(get_string_constant(*it), true);
 
     dest.add(goto_programt::make_other(fence, function.source_location()));
   }
@@ -1107,9 +1103,8 @@ void goto_convertt::do_function_call_symbol(
         function.source_location());
       rhs.copy_to_operands(list_arg);
       rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
-      goto_programt::targett t1=dest.add_instruction(ASSIGN);
-      t1->source_location=function.source_location();
-      t1->code=code_assignt(list_arg, rhs);
+      dest.add(goto_programt::make_assignment(
+        list_arg, rhs, function.source_location()));
     }
 
     if(lhs.is_not_nil())
@@ -1117,9 +1112,8 @@ void goto_convertt::do_function_call_symbol(
       typet t=pointer_type(lhs.type());
       dereference_exprt rhs(typecast_exprt(list_arg, t), lhs.type());
       rhs.add_source_location()=function.source_location();
-      goto_programt::targett t2=dest.add_instruction(ASSIGN);
-      t2->source_location=function.source_location();
-      t2->code=code_assignt(lhs, rhs);
+      dest.add(
+        goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
   }
   else if(identifier=="__builtin_va_copy")
@@ -1142,9 +1136,8 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    goto_programt::targett t=dest.add_instruction(ASSIGN);
-    t->source_location=function.source_location();
-    t->code=code_assignt(dest_expr, src_expr);
+    dest.add(goto_programt::make_assignment(
+      dest_expr, src_expr, function.source_location()));
   }
   else if(identifier=="__builtin_va_start")
   {
@@ -1169,9 +1162,8 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    goto_programt::targett t=dest.add_instruction(ASSIGN);
-    t->source_location=function.source_location();
-    t->code=code_assignt(dest_expr, src_expr);
+    dest.add(goto_programt::make_assignment(
+      dest_expr, src_expr, function.source_location()));
   }
   else if(identifier=="__builtin_va_end")
   {
@@ -1196,12 +1188,11 @@ void goto_convertt::do_function_call_symbol(
     // our __builtin_va_list is a pointer
     if(dest_expr.type().id() == ID_pointer)
     {
-      goto_programt::targett t=dest.add_instruction(ASSIGN);
-      t->source_location=function.source_location();
       const auto zero =
         zero_initializer(dest_expr.type(), function.source_location(), ns);
       CHECK_RETURN(zero.has_value());
-      t->code = code_assignt(dest_expr, *zero);
+      dest.add(goto_programt::make_assignment(
+        dest_expr, *zero, function.source_location()));
     }
   }
   else if(identifier=="__sync_fetch_and_add" ||
@@ -1233,17 +1224,14 @@ void goto_convertt::do_function_call_symbol(
     // build *ptr
     dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
 
-    goto_programt::targett t1=dest.add_instruction(ATOMIC_BEGIN);
-    t1->source_location=function.source_location();
+    dest.add(goto_programt::make_atomic_begin(function.source_location()));
 
     if(lhs.is_not_nil())
     {
       // return *ptr
-      goto_programt::targett t2=dest.add_instruction(ASSIGN);
-      t2->source_location=function.source_location();
-      t2->code=code_assignt(lhs, deref_ptr);
-      t2->code.op1() =
-        typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type());
+      exprt rhs = typecast_exprt::conditional_cast(deref_ptr, lhs.type());
+      dest.add(
+        goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
 
     irep_idt op_id=
@@ -1262,17 +1250,15 @@ void goto_convertt::do_function_call_symbol(
       typecast_exprt::conditional_cast(arguments[1], deref_ptr.type()),
       deref_ptr.type());
 
-    goto_programt::targett t3=dest.add_instruction(ASSIGN);
-    t3->source_location=function.source_location();
-    t3->code=code_assignt(deref_ptr, op_expr);
+    dest.add(goto_programt::make_assignment(
+      deref_ptr, op_expr, function.source_location()));
 
     // this instruction implies an mfence, i.e., WRfence
     codet fence(ID_fence);
     fence.set(ID_WRfence, true);
     dest.add(goto_programt::make_other(fence, function.source_location()));
 
-    goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
-    t5->source_location=function.source_location();
+    dest.add(goto_programt::make_atomic_end(function.source_location()));
   }
   else if(identifier=="__sync_add_and_fetch" ||
           identifier=="__sync_sub_and_fetch" ||
@@ -1303,8 +1289,7 @@ void goto_convertt::do_function_call_symbol(
     // build *ptr
     dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
 
-    goto_programt::targett t1=dest.add_instruction(ATOMIC_BEGIN);
-    t1->source_location=function.source_location();
+    dest.add(goto_programt::make_atomic_begin(function.source_location()));
 
     irep_idt op_id=
       identifier=="__sync_add_and_fetch"?ID_plus:
@@ -1322,18 +1307,15 @@ void goto_convertt::do_function_call_symbol(
       typecast_exprt::conditional_cast(arguments[1], deref_ptr.type()),
       deref_ptr.type());
 
-    goto_programt::targett t3=dest.add_instruction(ASSIGN);
-    t3->source_location=function.source_location();
-    t3->code=code_assignt(deref_ptr, op_expr);
+    dest.add(goto_programt::make_assignment(
+      deref_ptr, op_expr, function.source_location()));
 
     if(lhs.is_not_nil())
     {
       // return *ptr
-      goto_programt::targett t2=dest.add_instruction(ASSIGN);
-      t2->source_location=function.source_location();
-      t2->code=code_assignt(lhs, deref_ptr);
-      t2->code.op1() =
-        typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type());
+      exprt rhs = typecast_exprt::conditional_cast(deref_ptr, lhs.type());
+      dest.add(
+        goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
 
     // this instruction implies an mfence, i.e., WRfence
@@ -1341,8 +1323,7 @@ void goto_convertt::do_function_call_symbol(
     fence.set(ID_WRfence, true);
     dest.add(goto_programt::make_other(fence, function.source_location()));
 
-    goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
-    t5->source_location=function.source_location();
+    dest.add(goto_programt::make_atomic_end(function.source_location()));
   }
   else if(identifier=="__sync_bool_compare_and_swap")
   {
@@ -1377,8 +1358,7 @@ void goto_convertt::do_function_call_symbol(
     // build *ptr
     dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
 
-    goto_programt::targett t1=dest.add_instruction(ATOMIC_BEGIN);
-    t1->source_location=function.source_location();
+    dest.add(goto_programt::make_atomic_begin(function.source_location()));
 
     // build *ptr==oldval
     equal_exprt equal(
@@ -1388,11 +1368,9 @@ void goto_convertt::do_function_call_symbol(
     if(lhs.is_not_nil())
     {
       // return *ptr==oldval
-      goto_programt::targett t2=dest.add_instruction(ASSIGN);
-      t2->source_location=function.source_location();
-      t2->code=code_assignt(lhs, equal);
-      t2->code.op1() =
-        typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type());
+      exprt rhs = typecast_exprt::conditional_cast(equal, lhs.type());
+      dest.add(
+        goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
 
     // build (*ptr==oldval)?newval:*ptr
@@ -1402,16 +1380,15 @@ void goto_convertt::do_function_call_symbol(
       deref_ptr,
       deref_ptr.type());
 
-    goto_programt::targett t3=dest.add_instruction(ASSIGN);
-    t3->source_location=function.source_location();
-    t3->code=code_assignt(deref_ptr, if_expr);
+    dest.add(goto_programt::make_assignment(
+      deref_ptr, if_expr, function.source_location()));
 
     // this instruction implies an mfence, i.e., WRfence
     codet fence(ID_fence);
     fence.set(ID_WRfence, true);
     dest.add(goto_programt::make_other(fence, function.source_location()));
 
-    goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
+    goto_programt::targett t5 = dest.add(goto_programt::make_atomic_end());
     t5->source_location=function.source_location();
   }
   else if(identifier=="__sync_val_compare_and_swap")
@@ -1437,17 +1414,14 @@ void goto_convertt::do_function_call_symbol(
     // build *ptr
     dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
 
-    goto_programt::targett t1=dest.add_instruction(ATOMIC_BEGIN);
-    t1->source_location=function.source_location();
+    dest.add(goto_programt::make_atomic_begin(function.source_location()));
 
     if(lhs.is_not_nil())
     {
       // return *ptr
-      goto_programt::targett t2=dest.add_instruction(ASSIGN);
-      t2->source_location=function.source_location();
-      t2->code=code_assignt(lhs, deref_ptr);
-      t2->code.op1() =
-        typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type());
+      exprt rhs = typecast_exprt::conditional_cast(deref_ptr, lhs.type());
+      dest.add(
+        goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
 
     // build *ptr==oldval
@@ -1462,17 +1436,15 @@ void goto_convertt::do_function_call_symbol(
       deref_ptr,
       deref_ptr.type());
 
-    goto_programt::targett t3=dest.add_instruction(ASSIGN);
-    t3->source_location=function.source_location();
-    t3->code=code_assignt(deref_ptr, if_expr);
+    dest.add(goto_programt::make_assignment(
+      deref_ptr, if_expr, function.source_location()));
 
     // this instruction implies an mfence, i.e., WRfence
     codet fence(ID_fence);
     fence.set(ID_WRfence, true);
     dest.add(goto_programt::make_other(fence, function.source_location()));
 
-    goto_programt::targett t5=dest.add_instruction(ATOMIC_END);
-    t5->source_location=function.source_location();
+    dest.add(goto_programt::make_atomic_end(function.source_location()));
   }
   else if(identifier=="__sync_lock_test_and_set")
   {
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index e17f6a0dd65..81e457f9503 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -906,16 +906,15 @@ void goto_convertt::convert_for(
 
   // do the z label
   goto_programt tmp_z;
-  goto_programt::targett z=tmp_z.add_instruction(SKIP);
-  z->source_location=code.source_location();
+  goto_programt::targett z =
+    tmp_z.add(goto_programt::make_skip(code.source_location()));
 
   // do the x label
   goto_programt tmp_x;
 
   if(code.iter().is_nil())
   {
-    tmp_x.add_instruction(SKIP);
-    tmp_x.instructions.back().source_location=code.source_location();
+    tmp_x.add(goto_programt::make_skip(code.source_location()));
   }
   else
   {
@@ -924,10 +923,7 @@ void goto_convertt::convert_for(
     clean_expr(tmp_B, tmp_x, mode, false);
 
     if(tmp_x.instructions.empty())
-    {
-      tmp_x.add_instruction(SKIP);
-      tmp_x.instructions.back().source_location=code.source_location();
-    }
+      tmp_x.add(goto_programt::make_skip(code.source_location()));
   }
 
   // optimize the v label
@@ -948,8 +944,8 @@ void goto_convertt::convert_for(
 
   // y: goto u;
   goto_programt tmp_y;
-  goto_programt::targett y=tmp_y.add_instruction();
-  *y = goto_programt::make_goto(u, true_exprt(), code.source_location());
+  goto_programt::targett y = tmp_y.add(
+    goto_programt::make_goto(u, true_exprt(), code.source_location()));
 
   // loop invariant
   convert_loop_invariant(code, y, mode);
diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp
index f99e6158d3f..db774b8a02b 100644
--- a/src/goto-programs/goto_convert_exceptions.cpp
+++ b/src/goto-programs/goto_convert_exceptions.cpp
@@ -24,7 +24,7 @@ void goto_convertt::convert_msc_try_finally(
     code.find_source_location());
 
   goto_programt tmp;
-  tmp.add_instruction(SKIP)->source_location=code.source_location();
+  tmp.add(goto_programt::make_skip(code.source_location()));
 
   {
     // save 'leave' target
@@ -153,7 +153,7 @@ void goto_convertt::convert_CPROVER_try_catch(
 
   // this is where we go after 'throw'
   goto_programt tmp;
-  tmp.add_instruction(SKIP)->source_location=code.source_location();
+  tmp.add(goto_programt::make_skip(code.source_location()));
 
   // set 'throw' target
   throw_targett throw_target(targets);
@@ -183,13 +183,8 @@ void goto_convertt::convert_CPROVER_throw(
   const irep_idt &mode)
 {
   // set the 'exception' flag
-  {
-    goto_programt::targett t_set_exception=
-      dest.add_instruction(ASSIGN);
-
-    t_set_exception->source_location=code.source_location();
-    t_set_exception->code = code_assignt(exception_flag(mode), true_exprt());
-  }
+  dest.add(goto_programt::make_assignment(
+    exception_flag(mode), true_exprt(), code.source_location()));
 
   // do we catch locally?
   if(targets.throw_set)
diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/goto-programs/goto_convert_function_call.cpp
index 299dd28f0ad..1e23736e11a 100644
--- a/src/goto-programs/goto_convert_function_call.cpp
+++ b/src/goto-programs/goto_convert_function_call.cpp
@@ -129,7 +129,7 @@ void goto_convertt::do_function_call_if(
   do_function_call(lhs, function.false_case(), arguments, tmp_y, mode);
 
   if(tmp_y.instructions.empty())
-    y=tmp_y.add_instruction(SKIP);
+    y = tmp_y.add(goto_programt::make_skip());
   else
     y=tmp_y.instructions.begin();
 
@@ -143,7 +143,7 @@ void goto_convertt::do_function_call_if(
   do_function_call(lhs, function.true_case(), arguments, tmp_w, mode);
 
   if(tmp_w.instructions.empty())
-    tmp_w.add_instruction(SKIP);
+    tmp_w.add(goto_programt::make_skip());
 
   // x: goto z;
   *x = goto_programt::make_goto(z, true_exprt());
@@ -162,11 +162,8 @@ void goto_convertt::do_function_call_other(
   goto_programt &dest)
 {
   // don't know what to do with it
-  goto_programt::targett t=dest.add_instruction(FUNCTION_CALL);
-
   code_function_callt function_call(lhs, function, arguments);
   function_call.add_source_location()=function.source_location();
-
-  t->source_location=function.source_location();
-  t->code.swap(function_call);
+  dest.add(goto_programt::make_function_call(
+    function_call, function.source_location()));
 }
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index c3e4776b06d..96dbd04eef4 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -116,9 +116,7 @@ void goto_inlinet::parameter_assignments(
       code_assignt assignment(symbol_exprt(identifier, parameter_type), actual);
       assignment.add_source_location()=source_location;
 
-      dest.add_instruction(ASSIGN);
-      dest.instructions.back().source_location=source_location;
-      dest.instructions.back().code.swap(assignment);
+      dest.add(goto_programt::make_assignment(assignment, source_location));
     }
 
     if(it1!=arguments.end())
diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp
index d7a635f2dc0..8aff8b877a0 100644
--- a/src/goto-programs/remove_calls_no_body.cpp
+++ b/src/goto-programs/remove_calls_no_body.cpp
@@ -47,9 +47,7 @@ void remove_calls_no_bodyt::remove_call_no_body(
     code_assignt code(lhs, rhs);
     code.add_source_location() = target->source_location;
 
-    goto_programt::targett t = tmp.add_instruction(ASSIGN);
-    t->source_location = target->source_location;
-    t->code.swap(code);
+    tmp.add(goto_programt::make_assignment(code, target->source_location));
   }
 
   // kill call