use goto_progamt::make_X API

This prevents partial construction of instructiont.

Author: Daniel Kroening

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -124,9 +124,8 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
 
     // Insert an instruction declaring `aux_symbol` before `target`, being
     // careful to preserve jumps to `target`
-    goto_programt::instructiont decl_aux_symbol;
-    decl_aux_symbol.make_decl(code_declt(aux_symbol_expr));
-    decl_aux_symbol.source_location = source_loc;
+    goto_programt::instructiont decl_aux_symbol =
+      goto_programt::make_decl(code_declt(aux_symbol_expr), source_loc);
     goto_program.insert_before_swap(target, decl_aux_symbol);
 
     // Keep track of the new location of the instruction containing op.
@@ -142,10 +141,8 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
         mode);
     goto_program.destructive_insert(target2, gen_nondet_init_instructions);
 
-    goto_programt::targett dead_aux_symbol = goto_program.insert_after(target2);
-    dead_aux_symbol->make_dead();
-    dead_aux_symbol->code = code_deadt(aux_symbol_expr);
-    dead_aux_symbol->source_location = source_loc;
+    goto_program.insert_after(
+      target2, goto_programt::make_dead(aux_symbol_expr, source_loc));
 
     // In theory target could have more than one operand which should be
     // replaced by convert_nondet, so we return target2 so that it

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -233,22 +233,23 @@ void remove_exceptionst::instrument_exception_handler(
     null_pointer_exprt null_voidptr((pointer_type(java_void_type())));
 
     // add the assignment @inflight_exception = NULL
-    goto_programt::targett t_null=goto_program.insert_after(instr_it);
-    t_null->make_assignment();
-    t_null->source_location=instr_it->source_location;
-    t_null->code=code_assignt(
-      thrown_global_symbol,
-      null_voidptr);
+    goto_program.insert_after(
+      instr_it,
+      goto_programt::make_assignment(
+        code_assignt(thrown_global_symbol, null_voidptr),
+        instr_it->source_location));
 
     // add the assignment exc = @inflight_exception (before the null assignment)
-    goto_programt::targett t_exc=goto_program.insert_after(instr_it);
-    t_exc->make_assignment();
-    t_exc->source_location=instr_it->source_location;
-    t_exc->code=code_assignt(
-      thrown_exception_local,
-      typecast_exprt(thrown_global_symbol, thrown_exception_local.type()));
+    goto_program.insert_after(
+      instr_it,
+      goto_programt::make_assignment(
+        code_assignt(
+          thrown_exception_local,
+          typecast_exprt(thrown_global_symbol, thrown_exception_local.type())),
+        instr_it->source_location));
   }
-  instr_it->make_skip();
+
+  instr_it->turn_into_skip();
 }
 
 /// Find the innermost universal exception handler for the current
@@ -349,9 +350,10 @@ void remove_exceptionst::add_exception_dispatch_sequence(
       if(!stack_catch[i][j].first.empty())
       {
         // Normal exception handler, make an instanceof check.
-        goto_programt::targett t_exc=goto_program.insert_after(instr_it);
-        t_exc->make_goto(new_state_pc, true_exprt());
-        t_exc->source_location=instr_it->source_location;
+        goto_programt::targett t_exc = goto_program.insert_after(
+          instr_it,
+          goto_programt::make_goto(
+            new_state_pc, true_exprt(), instr_it->source_location));
 
         // use instanceof to check that this is the correct handler
         struct_tag_typet type(stack_catch[i][j].first);
@@ -374,16 +376,14 @@ void remove_exceptionst::add_exception_dispatch_sequence(
     }
   }
 
-  default_dispatch->make_goto(default_target, true_exprt());
-  default_dispatch->source_location=instr_it->source_location;
+  *default_dispatch = goto_programt::make_goto(
+    default_target, true_exprt(), instr_it->source_location);
 
   // add dead instructions
   for(const auto &local : locals)
   {
-    goto_programt::targett t_dead=goto_program.insert_after(instr_it);
-    t_dead->make_dead();
-    t_dead->code=code_deadt(local);
-    t_dead->source_location=instr_it->source_location;
+    goto_program.insert_after(
+      instr_it, goto_programt::make_dead(local, instr_it->source_location));
   }
 }
 
@@ -451,18 +451,22 @@ bool remove_exceptionst::instrument_function_call(
     {
       // Function is annotated must-not-throw, but we can't prove that here.
       // Insert an ASSUME(@inflight_exception == null):
-      goto_programt::targett assume_null = goto_program.insert_after(instr_it);
-      assume_null->make_assumption(no_exception_currently_in_flight);
+      goto_program.insert_after(
+        instr_it,
+        goto_programt::make_assumption(no_exception_currently_in_flight));
     }
     else
     {
       add_exception_dispatch_sequence(
         function_identifier, goto_program, instr_it, stack_catch, locals);
 
       // add a null check (so that instanceof can be applied)
-      goto_programt::targett t_null=goto_program.insert_after(instr_it);
-      t_null->make_goto(next_it, no_exception_currently_in_flight);
-      t_null->source_location=instr_it->source_location;
+      goto_program.insert_after(
+        instr_it,
+        goto_programt::make_goto(
+          next_it,
+          no_exception_currently_in_flight,
+          instr_it->source_location));
     }
 
     return true;
@@ -566,7 +570,8 @@ void remove_exceptionst::instrument_exceptions(
           false,
           "CATCH opcode should be one of push-catch, pop-catch, landingpad");
       }
-      instr_it->make_skip();
+
+      instr_it->turn_into_skip();
       did_something = true;
     }
     else if(instr_it->type==THROW)

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->make_skip();
+    *target = goto_programt::make_skip();
     // Actually alter the now-moved instruction:
     ++target;
   }

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -94,20 +94,19 @@ goto_programt::targett remove_java_newt::lower_java_new(
   malloc_expr.copy_to_operands(object_size);
   // could use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
-  target->make_assignment(code_assignt(lhs, malloc_expr));
-  target->source_location = location;
+  *target =
+    goto_programt::make_assignment(code_assignt(lhs, malloc_expr), location);
 
   // zero-initialize the object
   dereference_exprt deref(lhs, object_type);
   auto zero_object = zero_initializer(object_type, location, ns);
   CHECK_RETURN(zero_object.has_value());
   set_class_identifier(
     to_struct_expr(*zero_object), ns, to_struct_tag_type(object_type));
-  goto_programt::targett t_i = dest.insert_after(target);
-  t_i->make_assignment(code_assignt(deref, *zero_object));
-  t_i->source_location = location;
-
-  return t_i;
+  return dest.insert_after(
+    target,
+    goto_programt::make_assignment(
+      code_assignt(deref, *zero_object), location));
 }
 
 /// Replaces the instruction `lhs = new java_array_type` by
@@ -148,8 +147,8 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   // code use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
 
-  target->make_assignment(code_assignt(lhs, malloc_expr));
-  target->source_location = location;
+  *target =
+    goto_programt::make_assignment(code_assignt(lhs, malloc_expr), location);
   goto_programt::targett next = std::next(target);
 
   const struct_typet &struct_type = to_struct_type(ns.follow(object_type));
@@ -165,18 +164,19 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   CHECK_RETURN(zero_object.has_value());
   set_class_identifier(
     to_struct_expr(*zero_object), ns, to_struct_tag_type(object_type));
-  goto_programt::targett t_i = dest.insert_before(next);
-  t_i->make_assignment(code_assignt(deref, *zero_object));
-  t_i->source_location = location;
+  dest.insert_before(
+    next,
+    goto_programt::make_assignment(
+      code_assignt(deref, *zero_object), location));
 
   // if it's an array, we need to set the length field
   member_exprt length(
     deref,
     struct_type.components()[1].get_name(),
     struct_type.components()[1].type());
-  goto_programt::targett t_s = dest.insert_before(next);
-  t_s->make_assignment(code_assignt(length, rhs.op0()));
-  t_s->source_location = location;
+  dest.insert_before(
+    next,
+    goto_programt::make_assignment(code_assignt(length, rhs.op0()), location));
 
   // we also need to allocate space for the data
   member_exprt data(
@@ -221,20 +221,19 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
                                          .symbol_expr();
   code_declt array_decl(new_array_data_symbol);
   array_decl.add_source_location() = location;
-  goto_programt::targett t_array_decl = dest.insert_before(next);
-  t_array_decl->make_decl(array_decl);
-  t_array_decl->source_location = location;
-  goto_programt::targett t_p2 = dest.insert_before(next);
-  t_p2->make_assignment(
-    code_assignt(new_array_data_symbol, data_java_new_expr));
-  t_p2->source_location = location;
-
-  goto_programt::targett t_p = dest.insert_before(next);
+  dest.insert_before(next, goto_programt::make_decl(array_decl, location));
+  dest.insert_before(
+    next,
+    goto_programt::make_assignment(
+      code_assignt(new_array_data_symbol, data_java_new_expr), location));
+
   exprt cast_java_new = new_array_data_symbol;
   if(cast_java_new.type() != data.type())
     cast_java_new = typecast_exprt(cast_java_new, data.type());
-  t_p->make_assignment(code_assignt(data, cast_java_new));
-  t_p->source_location = location;
+  dest.insert_before(
+    next,
+    goto_programt::make_assignment(
+      code_assignt(data, cast_java_new), location));
 
   // zero-initialize the data
   if(!rhs.get_bool(ID_skip_initialize))
@@ -244,9 +243,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     CHECK_RETURN(zero_element.has_value());
     codet array_set(ID_array_set);
     array_set.copy_to_operands(new_array_data_symbol, *zero_element);
-    goto_programt::targett t_d = dest.insert_before(next);
-    t_d->make_other(array_set);
-    t_d->source_location = location;
+    dest.insert_before(next, goto_programt::make_other(array_set, location));
   }
 
   // multi-dimensional?
@@ -265,9 +262,8 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
         .symbol_expr();
     code_declt decl(tmp_i);
     decl.add_source_location() = location;
-    goto_programt::targett t_decl = tmp.insert_before(tmp.instructions.begin());
-    t_decl->make_decl(decl);
-    t_decl->source_location = location;
+    tmp.insert_before(
+      tmp.instructions.begin(), goto_programt::make_decl(decl, location));
 
     side_effect_exprt sub_java_new = rhs;
     sub_java_new.operands().erase(sub_java_new.operands().begin());

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -271,7 +271,7 @@ static goto_programt::targett check_and_replace_target(
 
   std::for_each(
     target, target_instruction, [](goto_programt::instructiont &instr) {
-      instr.make_skip();
+      instr.turn_into_skip();
     });
 
   if(target_instruction->is_return())

src/analyses/escape_analysis.cpp

@@ -427,8 +427,7 @@ void escape_analysist::insert_cleanup(
       code.arguments().push_back(arg);
     }
 
-    location->make_function_call(code);
-    location->source_location=source_location;
+    *location = goto_programt::make_function_call(code, source_location);
   }
 }
 

src/analyses/goto_check.cpp

@@ -1801,15 +1801,15 @@ void goto_checkt::goto_check(
           i.source_location.get_property_class()!="error label") ||
          (!is_user_provided && !enable_built_in_assertions))
       {
-        i.make_skip();
+        i.turn_into_skip();
         did_something = true;
       }
     }
     else if(i.is_assume())
     {
       if(!enable_assumptions)
       {
-        i.make_skip();
+        i.turn_into_skip();
         did_something = true;
       }
     }

src/analyses/interval_analysis.cpp

@@ -79,7 +79,7 @@ void instrument_intervals(
     {
       goto_programt::targett t=i_it;
       goto_function.body.insert_before_swap(i_it);
-      t->make_assumption(conjunction(assertion));
+      *t = goto_programt::make_assumption(conjunction(assertion));
       i_it++; // goes to original instruction
       t->source_location=i_it->source_location;
     }

src/assembler/remove_asm.cpp

@@ -495,7 +495,7 @@ void remove_asmt::process_function(
     {
       goto_programt tmp_dest;
       process_instruction(*it, tmp_dest);
-      it->make_skip();
+      it->turn_into_skip();
       did_something = true;
 
       goto_programt::targett next = it;

src/goto-analyzer/taint_analysis.cpp

@@ -166,21 +166,20 @@ void taint_analysist::instrument(
                   code_set_may.op0()=where;
                   code_set_may.op1()=
                     address_of_exprt(string_constantt(rule.taint));
-                  goto_programt::targett t=insert_after.add_instruction();
-                  t->make_other(code_set_may);
-                  t->source_location=instruction.source_location;
+                  insert_after.add(goto_programt::make_other(
+                    code_set_may, instruction.source_location));
                 }
                 break;
 
               case taint_parse_treet::rulet::SINK:
                 {
-                  goto_programt::targett t=insert_before.add_instruction();
                   binary_predicate_exprt get_may(
                     where,
                     "get_may",
                     address_of_exprt(string_constantt(rule.taint)));
-                  t->make_assertion(not_exprt(get_may));
-                  t->source_location=instruction.source_location;
+                  goto_programt::targett t =
+                    insert_before.add(goto_programt::make_assertion(
+                      not_exprt(get_may), instruction.source_location));
                   t->source_location.set_property_class(
                     "taint rule "+id2string(rule.id));
                   t->source_location.set_comment(rule.message);
@@ -194,9 +193,8 @@ void taint_analysist::instrument(
                   code_clear_may.op0()=where;
                   code_clear_may.op1()=
                     address_of_exprt(string_constantt(rule.taint));
-                  goto_programt::targett t=insert_after.add_instruction();
-                  t->make_other(code_clear_may);
-                  t->source_location=instruction.source_location;
+                  insert_after.add(goto_programt::make_other(
+                    code_clear_may, instruction.source_location));
                 }
                 break;
               }
@@ -285,14 +283,13 @@ bool taint_analysist::operator()(
            f_it->first!=goto_functionst::entry_point())
         {
           const symbolt &symbol = ns.lookup(f_it->first);
-          goto_programt::targett t=calls.add_instruction();
           const code_function_callt call(symbol.symbol_expr());
-          t->make_function_call(call);
-          calls.add_instruction()->make_goto(
-            end.instructions.begin(), true_exprt());
-          goto_programt::targett g=gotos.add_instruction();
-          g->make_goto(
-            t, side_effect_expr_nondett(bool_typet(), symbol.location));
+          goto_programt::targett t =
+            calls.add(goto_programt::make_function_call(call));
+          calls.add(
+            goto_programt::make_goto(end.instructions.begin(), true_exprt()));
+          gotos.add(goto_programt::make_goto(
+            t, side_effect_expr_nondett(bool_typet(), symbol.location)));
         }
 
       goto_functionst::goto_functiont &entry=