diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 40f27299f95..7936e9bb16b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/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 java_bytecode_instrumentt::instrument_expr(const exprt &expr) forall_operands(it, expr) { if(optionalt 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 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 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 diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 465fb281883..b4af4eeac59 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/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); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 44b9af5935d..e7e9217d4ed 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/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 diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 265954a003f..4115cda5e9b 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/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, diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index 34673a85181..2186299a7de 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/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()); diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 27c8e3b2d8d..41fd9618811 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/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 diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 9f6e1bbcd9c..15e1a712f51 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -117,7 +117,7 @@ exprt symbol_factoryt::allocate_object( // = &tmp$ 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; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 504b3568992..93ac22ca07a 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/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 } diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index fd584500f28..09558d6063a 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -116,7 +116,7 @@ optionalt 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 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 diff --git a/src/util/nondet.cpp b/src/util/nondet.cpp index 8e9e1835ad2..50bb3069b50 100644 --- a/src/util/nondet.cpp +++ b/src/util/nondet.cpp @@ -95,7 +95,6 @@ code_blockt generate_nondet_switch( if(switch_cases.size() == 1) return code_blockt({switch_cases[0]}); - code_switcht result_switch; code_blockt result_block; const symbol_exprt &switch_value = generate_nondet_int( @@ -108,8 +107,6 @@ code_blockt generate_nondet_switch( symbol_table, result_block); - result_switch.value() = switch_value; - code_blockt switch_block; size_t case_number = 0; for(const auto &switch_case : switch_cases) @@ -117,14 +114,13 @@ code_blockt generate_nondet_switch( code_blockt this_block; this_block.add(switch_case); this_block.add(code_breakt()); - code_switch_caset this_case; - this_case.case_op() = from_integer(case_number, switch_value.type()); - this_case.code() = this_block; - switch_block.move(this_case); + code_switch_caset this_case( + from_integer(case_number, switch_value.type()), this_block); + switch_block.add(std::move(this_case)); ++case_number; } - result_switch.body() = switch_block; - result_block.move(result_switch); + code_switcht result_switch(switch_value, switch_block); + result_block.add(std::move(result_switch)); return result_block; } diff --git a/src/util/std_code.h b/src/util/std_code.h index 1b1356fc2cc..2de906428bd 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -137,11 +137,6 @@ class code_blockt:public codet operands()=std::move((std::vector &&)_statements); } - void move(codet &code) - { - move_to_operands(code); - } - void add(const codet &code) { add_to_operands(code);