Merge pull request diffblue#3505 from tautschnig/constructors-for

Add a four-operand constructor to code_fort

Author: chrisr-diffblue

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -897,25 +897,21 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
     code_declt declare_index(index_symexpr);
 
-    code_fort copy_loop;
-
-    copy_loop.init()=
-      code_assignt(index_symexpr, from_integer(0, index_symexpr.type()));
-    copy_loop.cond()=
-      binary_relation_exprt(index_symexpr, ID_lt, old_length);
-
     side_effect_exprt inc(ID_assign, typet(), location);
     inc.operands().resize(2);
     inc.op0()=index_symexpr;
     inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
-    copy_loop.iter()=inc;
 
     dereference_exprt old_cell(
       plus_exprt(old_data, index_symexpr), old_data.type().subtype());
     dereference_exprt new_cell(
       plus_exprt(new_data, index_symexpr), new_data.type().subtype());
-    code_assignt copy_cell(new_cell, old_cell);
-    copy_loop.body()=copy_cell;
+
+    const code_fort copy_loop(
+      code_assignt(index_symexpr, from_integer(0, index_symexpr.type())),
+      binary_relation_exprt(index_symexpr, ID_lt, old_length),
+      std::move(inc),
+      code_assignt(std::move(new_cell), std::move(old_cell)));
 
     member_exprt new_base_class(
       new_array, base_class_component.get_name(), base_class_component.type());

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -266,8 +266,6 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     t_decl->make_decl(decl);
     t_decl->source_location = location;
 
-    code_fort for_loop;
-
     side_effect_exprt sub_java_new = rhs;
     sub_java_new.operands().erase(sub_java_new.operands().begin());
 
@@ -304,10 +302,11 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
       deref_expr, typecast_exprt(init_sym, deref_expr.type()));
     for_body.add(std::move(assign_subarray));
 
-    for_loop.init() = code_assignt(tmp_i, from_integer(0, tmp_i.type()));
-    for_loop.cond() = binary_relation_exprt(tmp_i, ID_lt, rhs.op0());
-    for_loop.iter() = inc;
-    for_loop.body() = for_body;
+    const code_fort for_loop(
+      code_assignt(tmp_i, from_integer(0, tmp_i.type())),
+      binary_relation_exprt(tmp_i, ID_lt, rhs.op0()),
+      std::move(inc),
+      std::move(for_body));
 
     goto_convert(for_loop, symbol_table, tmp, get_message_handler(), ID_java);
 

src/ansi-c/expr2c.cpp

@@ -2801,16 +2801,16 @@ std::string expr2ct::convert_code_for(
   std::string dest=indent_str(indent);
   dest+="for(";
 
-  if(!src.op0().is_nil())
-    dest+=convert(src.op0());
+  if(!src.init().is_nil())
+    dest += convert(src.init());
   else
     dest+=' ';
   dest+="; ";
-  if(!src.op1().is_nil())
-    dest+=convert(src.op1());
+  if(!src.cond().is_nil())
+    dest += convert(src.cond());
   dest+="; ";
-  if(!src.op2().is_nil())
-    dest+=convert(src.op2());
+  if(!src.iter().is_nil())
+    dest += convert(src.iter());
 
   if(src.body().is_nil())
     dest+=");\n";

src/goto-instrument/goto_program2code.cpp

@@ -628,13 +628,8 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
   if(w.body().has_operands() &&
      to_code(w.body().operands().back()).get_statement()==ID_assign)
   {
-    code_fort f;
+    code_fort f(nil_exprt(), w.cond(), w.body().operands().back(), codet());
 
-    f.init().make_nil();
-
-    f.cond()=w.cond();
-
-    f.iter()=w.body().operands().back();
     w.body().operands().pop_back();
     f.iter().id(ID_side_effect);
 

src/goto-programs/goto_convert.cpp

@@ -952,7 +952,7 @@ void goto_convertt::convert_for(
   // do the x label
   goto_programt tmp_x;
 
-  if(code.op2().is_nil())
+  if(code.iter().is_nil())
   {
     tmp_x.add_instruction(SKIP);
     tmp_x.instructions.back().source_location=code.source_location();

src/util/std_code.h

@@ -882,6 +882,20 @@ class code_fort:public codet
     operands().resize(4);
   }
 
+  /// A statement describing a for loop with initializer \p _init, loop
+  /// condition \p _cond, increment \p _iter, and body \p _body.
+  code_fort(
+    const exprt &_init,
+    const exprt &_cond,
+    const exprt &_iter,
+    const codet &_body)
+    : codet(ID_for)
+  {
+    reserve_operands(4);
+    add_to_operands(_init, _cond, _iter);
+    add_to_operands(_body);
+  }
+
   // nil or a statement
   const exprt &init() const
   {