Merge pull request #3278 from tautschnig/no-codet-move

Replace uses of codet::move by codet::add(std::move(...)) [blocks: #2310]

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -329,7 +329,7 @@ void java_bytecode_instrumentt::add_expr_instrumentation(
     if(expr_instrumentation->get_statement() == ID_block)
       block.append(to_code_block(*expr_instrumentation));
     else
-      block.move(*expr_instrumentation);
+      block.add(std::move(*expr_instrumentation));
   }
 }
 
@@ -476,7 +476,7 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
   forall_operands(it, expr)
   {
     if(optionalt<codet> op_result = instrument_expr(*it))
-      result.move(*op_result);
+      result.add(std::move(*op_result));
   }
 
   // Add any check due at this node:
@@ -498,7 +498,7 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
             dereference_expr,
             plus_expr.op1(),
             expr.source_location());
-        result.move(bounds_check);
+        result.add(std::move(bounds_check));
       }
     }
   }
@@ -534,7 +534,7 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
       check_null_dereference(
         dereference_expr.op0(),
         dereference_expr.source_location());
-    result.move(null_dereference_check);
+    result.add(std::move(null_dereference_check));
   }
 
   if(result==code_blockt())
@@ -598,7 +598,7 @@ void java_bytecode_instrument_uncaught_exceptions(
   assert_location.set_comment("no uncaught exception");
   assert_no_exception.add_source_location() = assert_location;
 
-  init_code.move(assert_no_exception);
+  init_code.add(std::move(assert_no_exception));
 }
 
 /// Instruments all the code in the symbol_table with

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -204,10 +204,11 @@ static void java_static_lifetime_init(
         set_class_identifier(
           to_struct_expr(*zero_object), ns, to_symbol_type(sym.type));
 
-        code_block.add(code_assignt(sym.symbol_expr(), *zero_object));
+        code_block.add(
+          std::move(code_assignt(sym.symbol_expr(), *zero_object)));
 
         // Then call the init function:
-        code_block.move(initializer_call);
+        code_block.add(std::move(initializer_call));
       }
       else if(sym.value.is_nil() && sym.type!=empty_typet())
       {
@@ -415,7 +416,7 @@ exprt::operandst java_build_arguments(
     input.op1()=main_arguments[param_number];
     input.add_source_location()=function.location;
 
-    init_code.move(input);
+    init_code.add(std::move(input));
   }
 
   return main_arguments;
@@ -453,7 +454,7 @@ void java_record_outputs(
     output.op1()=return_symbol.symbol_expr();
     output.add_source_location()=function.location;
 
-    init_code.move(output);
+    init_code.add(std::move(output));
   }
 
   for(std::size_t param_number=0;
@@ -476,7 +477,7 @@ void java_record_outputs(
       output.op1()=main_arguments[param_number];
       output.add_source_location()=function.location;
 
-      init_code.move(output);
+      init_code.add(std::move(output));
     }
   }
 
@@ -494,7 +495,7 @@ void java_record_outputs(
   output.op1()=exc_symbol.symbol_expr();
   output.add_source_location()=function.location;
 
-  init_code.move(output);
+  init_code.add(std::move(output));
 }
 
 main_function_resultt get_main_symbol(
@@ -674,7 +675,7 @@ bool generate_java_start_function(
     code_function_callt call_init(init_it->second.symbol_expr());
     call_init.add_source_location()=symbol.location;
 
-    init_code.move(call_init);
+    init_code.add(std::move(call_init));
   }
 
   // build call to the main method, of the form
@@ -747,26 +748,26 @@ bool generate_java_start_function(
   irept catch_type_list(ID_exception_list);
   irept catch_target_list(ID_label);
 
-  call_block.move(push_universal_handler);
+  call_block.add(std::move(push_universal_handler));
 
   // we insert the call to the method AFTER the argument initialization code
-  call_block.move(call_main);
+  call_block.add(std::move(call_main));
 
   // Pop the handler:
   code_pop_catcht pop_handler;
-  call_block.move(pop_handler);
-  init_code.move(call_block);
+  call_block.add(std::move(pop_handler));
+  init_code.add(std::move(call_block));
 
   // Normal return: skip the exception handler:
   init_code.add(code_gotot(after_catch.get_label()));
 
   // Exceptional return: catch and assign to exc_symbol.
   code_landingpadt landingpad(exc_symbol.symbol_expr());
-  init_code.add(toplevel_catch);
-  init_code.move(landingpad);
+  init_code.add(std::move(toplevel_catch));
+  init_code.add(std::move(landingpad));
 
   // Converge normal and exceptional return:
-  init_code.move(after_catch);
+  init_code.add(std::move(after_catch));
 
   // declare certain (which?) variables as test outputs
   java_record_outputs(symbol, main_arguments, init_code, symbol_table);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1396,7 +1396,7 @@ void java_object_factoryt::gen_nondet_array_init(
   code_labelt init_head_label(head_name, code_skipt());
   code_gotot goto_head(head_name);
 
-  assignments.move(init_head_label);
+  assignments.add(std::move(init_head_label));
 
   std::string done_name = id2string(counter.base_name) + "_done";
   code_labelt init_done_label(done_name, code_skipt());
@@ -1406,7 +1406,7 @@ void java_object_factoryt::gen_nondet_array_init(
   done_test.cond()=equal_exprt(counter_expr, length_expr);
   done_test.then_case()=goto_done;
 
-  assignments.move(done_test);
+  assignments.add(std::move(done_test));
 
   if(update_in_place!=update_in_placet::MUST_UPDATE_IN_PLACE)
   {
@@ -1416,7 +1416,7 @@ void java_object_factoryt::gen_nondet_array_init(
     max_test.cond()=equal_exprt(counter_expr, max_length_expr);
     max_test.then_case()=goto_done;
 
-    assignments.move(max_test);
+    assignments.add(std::move(max_test));
   }
 
   const dereference_exprt arraycellref(
@@ -1447,9 +1447,9 @@ void java_object_factoryt::gen_nondet_array_init(
   exprt java_one=from_integer(1, java_int_type());
   code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
 
-  assignments.move(incr);
-  assignments.move(goto_head);
-  assignments.move(init_done_label);
+  assignments.add(std::move(incr));
+  assignments.add(std::move(goto_head));
+  assignments.add(std::move(init_done_label));
 }
 
 /// We nondet-initialize enums to be equal to one of the constants defined

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -687,9 +687,8 @@ code_ifthenelset get_clinit_wrapper_body(
   wrapper_body.cond() = check_already_run;
 
   // add the "already-run = false" statement
-  code_blockt init_body;
   code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
-  init_body.move(set_already_run);
+  code_blockt init_body({set_already_run});
 
   clinit_wrapper_do_recursive_calls(
     symbol_table,

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -296,13 +296,13 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
                               .symbol_expr();
     code_declt init_decl(init_sym);
     init_decl.add_source_location() = location;
-    for_body.move(init_decl);
+    for_body.add(std::move(init_decl));
 
     code_assignt init_subarray(init_sym, sub_java_new);
+    for_body.add(std::move(init_subarray));
     code_assignt assign_subarray(
       deref_expr, typecast_exprt(init_sym, deref_expr.type()));
-    for_body.move(init_subarray);
-    for_body.move(assign_subarray);
+    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());

src/ansi-c/ansi_c_entry_point.cpp

@@ -73,7 +73,7 @@ void record_function_outputs(
     output.op1()=return_symbol.symbol_expr();
     output.add_source_location()=function.location;
 
-    init_code.move(output);
+    init_code.add(std::move(output));
   }
 
   #if 0
@@ -101,7 +101,7 @@ void record_function_outputs(
       output.op1()=symbol.symbol_expr();
       output.add_source_location()=p.source_location();
 
-      init_code.move_to_operands(output);
+      init_code.add(std::move(output));
     }
 
     i++;
@@ -215,7 +215,7 @@ bool generate_ansi_c_start_function(
     code_function_callt call_init(init_it->second.symbol_expr());
     call_init.add_source_location()=symbol.location;
 
-    init_code.move(call_init);
+    init_code.add(std::move(call_init));
   }
 
   // build call to main function
@@ -260,7 +260,7 @@ bool generate_ansi_c_start_function(
         const binary_relation_exprt ge(argc_symbol.symbol_expr(), ID_ge, one);
 
         code_assumet assumption(ge);
-        init_code.move(assumption);
+        init_code.add(std::move(assumption));
       }
 
       {
@@ -274,7 +274,7 @@ bool generate_ansi_c_start_function(
           argc_symbol.symbol_expr(), ID_le, bound_expr);
 
         code_assumet assumption(le);
-        init_code.move(assumption);
+        init_code.add(std::move(assumption));
       }
 
       {
@@ -284,7 +284,7 @@ bool generate_ansi_c_start_function(
         input.op0()=address_of_exprt(
           index_exprt(string_constantt("argc"), from_integer(0, index_type())));
         input.op1()=argc_symbol.symbol_expr();
-        init_code.move(input);
+        init_code.add(std::move(input));
       }
 
       if(parameters.size()==3)
@@ -311,7 +311,7 @@ bool generate_ansi_c_start_function(
           envp_size_symbol.symbol_expr(), ID_le, max_minus_one);
 
         code_assumet assumption(le);
-        init_code.move(assumption);
+        init_code.add(std::move(assumption));
       }
 
       {
@@ -366,7 +366,7 @@ bool generate_ansi_c_start_function(
         const equal_exprt is_null(index_expr, null);
 
         code_assumet assumption2(is_null);
-        init_code.move(assumption2);
+        init_code.add(std::move(assumption2));
       }
 
       {
@@ -430,7 +430,7 @@ bool generate_ansi_c_start_function(
         symbol_table);
   }
 
-  init_code.move(call_main);
+  init_code.add(std::move(call_main));
 
   // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
 

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -117,7 +117,7 @@ exprt symbol_factoryt::allocate_object(
   //   <target_expr> = &tmp$<temporary_counter>
   code_assignt assign(target_expr, aoe);
   assign.add_source_location()=loc;
-  assignments.move(assign);
+  assignments.add(std::move(assign));
 
   return aoe;
 }
@@ -178,7 +178,7 @@ void symbol_factoryt::gen_nondet_init(
       null_check.then_case()=set_null_inst;
       null_check.else_case()=non_null_inst;
 
-      assignments.move(null_check);
+      assignments.add(std::move(null_check));
     }
   }
   // TODO(OJones): Add support for structs and arrays
@@ -193,7 +193,7 @@ void symbol_factoryt::gen_nondet_init(
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
 
-    assignments.move(assign);
+    assignments.add(std::move(assign));
   }
 }
 
@@ -249,7 +249,7 @@ symbol_exprt c_nondet_symbol_factory(
   {
     code_declt decl(symbol_ptr->symbol_expr());
     decl.add_source_location()=loc;
-    init_code.move(decl);
+    init_code.add(std::move(decl));
   }
 
   init_code.append(assignments);
@@ -266,7 +266,7 @@ symbol_exprt c_nondet_symbol_factory(
         from_integer(0, index_type())));
     input_code.op1()=symbol_ptr->symbol_expr();
     input_code.add_source_location()=loc;
-    init_code.move(input_code);
+    init_code.add(std::move(input_code));
   }
 
   return main_symbol_expr;

src/ansi-c/c_typecheck_code.cpp

@@ -433,7 +433,7 @@ void c_typecheck_baset::typecheck_for(codet &code)
         code_blockt code_block;
         code_block.add_source_location()=code.op3().source_location();
 
-        code_block.move(to_code(code.op3()));
+        code_block.add(std::move(to_code(code.op3())));
         code.op3().swap(code_block);
       }
       typecheck_code(to_code(code.op3()));
@@ -461,9 +461,9 @@ void c_typecheck_baset::typecheck_for(codet &code)
     }
 
     code_block.reserve_operands(2);
-    code_block.move(to_code(code.op0()));
+    code_block.add(std::move(to_code(code.op0())));
     code.op0().make_nil();
-    code_block.move(code);
+    code_block.add(std::move(code));
     code.swap(code_block);
     typecheck_code(code); // recursive call
   }

src/cpp/cpp_constructor.cpp

@@ -116,7 +116,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
         auto i_code = cpp_constructor(source_location, index, tmp_operands);
 
         if(i_code.has_value())
-          new_code.move(i_code.value());
+          new_code.add(std::move(i_code.value()));
       }
       return std::move(new_code);
     }
@@ -192,8 +192,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
       side_effect_exprt assign(ID_assign, typet(), source_location);
       assign.move_to_operands(member, val);
       typecheck_side_effect_assignment(assign);
-      code_expressiont code_exp(assign);
-      block.move(code_exp);
+      block.add(std::move(code_expressiont(assign)));
     }
 
     // enter struct scope