use make_assignment(lhs, rhs)

This is slightly shorter.

Author: Daniel Kroening

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

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

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;

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