use goto_programt::instructiont constructor

This ensures full initialization of the class.

Author: Daniel Kroening

src/analyses/goto_check.cpp

@@ -1438,13 +1438,16 @@ void goto_checkt::add_guarded_claim(
     goto_program_instruction_typet type=
       enable_assert_to_assume?ASSUME:ASSERT;
 
-    goto_programt::targett t=new_code.add_instruction(type);
+    goto_programt::targett t = new_code.add(goto_programt::instructiont(
+      static_cast<const codet &>(get_nil_irep()),
+      source_location,
+      type,
+      std::move(new_expr),
+      {}));
 
     std::string source_expr_string;
     get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
-    t->set_condition(std::move(new_expr));
-    t->source_location=source_location;
     t->source_location.set_comment(comment+" in "+source_expr_string);
     t->source_location.set_property_class(property_class);
   }
@@ -1739,10 +1742,13 @@ void goto_checkt::goto_check(
         goto_program_instruction_typet type=
           enable_assert_to_assume?ASSUME:ASSERT;
 
-        goto_programt::targett t=new_code.add_instruction(type);
+        goto_programt::targett t = new_code.add(goto_programt::instructiont(
+          static_cast<const codet &>(get_nil_irep()),
+          i.source_location,
+          type,
+          false_exprt(),
+          {}));
 
-        t->set_condition(false_exprt());
-        t->source_location=i.source_location;
         t->source_location.set_property_class("error label");
         t->source_location.set_comment("error label "+label);
         t->source_location.set("user-provided", true);

src/goto-instrument/unwind.cpp

@@ -48,8 +48,9 @@ void goto_unwindt::copy_segment(
 
   for(goto_programt::const_targett t=start; t!=end; t++)
   {
-    goto_programt::targett t_new=goto_program.add_instruction();
-    *t_new=*t;
+    // copy the instruction
+    goto_programt::targett t_new =
+      goto_program.add(goto_programt::instructiont(*t));
     unwind_log.insert(t_new, t->location_number);
     target_vector.push_back(t_new); // store copied instruction
   }

src/goto-programs/goto_convert_functions.cpp

@@ -182,9 +182,8 @@ void goto_convert_functionst::convert_function(
     end_location.make_nil();
 
   goto_programt tmp_end_function;
-  goto_programt::targett end_function=tmp_end_function.add_instruction();
-  end_function->type=END_FUNCTION;
-  end_function->source_location=end_location;
+  goto_programt::targett end_function =
+    tmp_end_function.add(goto_programt::make_end_function(end_location));
 
   targets=targetst();
   targets.set_return(end_function);

src/goto-programs/goto_convert_side_effect.cpp

@@ -594,13 +594,12 @@ void goto_convertt::remove_side_effect(
   }
   else if(statement==ID_throw)
   {
-    goto_programt::targett t=dest.add_instruction(THROW);
-    t->code = code_expressiont(
-      side_effect_expr_throwt(
-        expr.find(ID_exception_list), expr.type(), expr.source_location()));
-    t->code.op0().operands().swap(expr.operands());
-    t->code.add_source_location()=expr.source_location();
-    t->source_location=expr.source_location();
+    codet code = code_expressiont(side_effect_expr_throwt(
+      expr.find(ID_exception_list), expr.type(), expr.source_location()));
+    code.op0().operands().swap(expr.operands());
+    code.add_source_location() = expr.source_location();
+    dest.add(goto_programt::instructiont(
+      std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
 
     // the result can't be used, these are void
     expr.make_nil();

src/goto-programs/string_instrumentation.cpp

@@ -833,24 +833,7 @@ void string_instrumentationt::invalidate_buffer(
     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;
-
-  const plus_exprt plus(
-    cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
-
-  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));
-
-  goto_programt::targett exit =
-    dest.add(goto_programt::make_skip(target->source_location));
-
-  exprt cnt_bs, bufp;
+  exprt bufp;
 
   if(buf_type.id()==ID_pointer)
     bufp=buffer;
@@ -861,9 +844,6 @@ void string_instrumentationt::invalidate_buffer(
     bufp=address_of_exprt(index);
   }
 
-  const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
-  const dereference_exprt deref(b_plus_i, buf_type.subtype());
-
   exprt condition;
 
   if(limit==0)
@@ -873,7 +853,32 @@ void string_instrumentationt::invalidate_buffer(
     condition = binary_relation_exprt(
       cntr_sym.symbol_expr(), ID_gt, from_integer(limit, unsigned_int_type()));
 
-  *check = goto_programt::make_goto(exit, condition, target->source_location);
+  goto_programt::targett check = dest.add(
+    goto_programt::make_incomplete_goto(condition, target->source_location));
+
+  goto_programt::targett invalidate = dest.add(goto_programt::instructiont(
+    static_cast<const codet &>(get_nil_irep()),
+    target->source_location,
+    ASSIGN,
+    nil_exprt(),
+    {}));
+
+  const plus_exprt plus(
+    cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
+
+  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));
+
+  goto_programt::targett exit =
+    dest.add(goto_programt::make_skip(target->source_location));
+
+  check->complete_goto(exit);
+
+  const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
+  const dereference_exprt deref(b_plus_i, buf_type.subtype());
 
   const side_effect_expr_nondett nondet(
     buf_type.subtype(), target->source_location);