diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index c74e508d933..849d5565558 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -280,8 +280,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array( const auto zero_element = zero_initializer(data.type().subtype(), location, ns); CHECK_RETURN(zero_element.has_value()); - codet array_set(ID_array_set); - array_set.copy_to_operands(new_array_data_symbol, *zero_element); + codet array_set{ID_array_set, {new_array_data_symbol, *zero_element}}; dest.insert_before(next, goto_programt::make_other(array_set, location)); } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 82fc855c68a..9f377702292 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1035,8 +1035,8 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) // It is not obvious whether the type or 'e' should be evaluated // first. - exprt comma_expr(ID_comma, expr.type()); - comma_expr.copy_to_operands(side_effect_expr, expr); + binary_exprt comma_expr{ + std::move(side_effect_expr), ID_comma, expr, expr.type()}; expr.swap(comma_expr); } } @@ -1085,8 +1085,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr) // It is not obvious whether the type or 'e' should be evaluated // first. - exprt comma_expr(ID_comma, op.type()); - comma_expr.copy_to_operands(side_effect_expr, op); + binary_exprt comma_expr{ + std::move(side_effect_expr), ID_comma, op, op.type()}; op.swap(comma_expr); } diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index a154338c099..6e3c59c89e0 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -100,7 +100,7 @@ void goto_convertt::do_prob_uniform( throw 0; } - rhs.copy_to_operands(arguments[0], arguments[1]); + rhs.add_to_operands(exprt{arguments[0]}, exprt{arguments[1]}); code_assignt assignment(lhs, rhs); assignment.add_source_location()=function.source_location(); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 2a5785b1eb9..dd24393cbe6 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -112,29 +112,23 @@ void goto_convertt::remove_assignment( UNREACHABLE; } - exprt rhs; - - const typet &op0_type = to_binary_expr(expr).op0().type(); + const binary_exprt &binary_expr = to_binary_expr(expr); + const typet &op0_type = binary_expr.op0().type(); PRECONDITION( op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum && op0_type.id() != ID_c_bool && op0_type.id() != ID_bool); - rhs.id(new_id); - rhs.copy_to_operands( - to_binary_expr(expr).op0(), to_binary_expr(expr).op1()); - rhs.type() = to_binary_expr(expr).op0().type(); + exprt rhs = binary_exprt{binary_expr.op0(), new_id, binary_expr.op1()}; rhs.add_source_location() = expr.source_location(); - if( - result_is_used && !address_taken && - needs_cleaning(to_binary_expr(expr).op0())) + if(result_is_used && !address_taken && needs_cleaning(binary_expr.op0())) { make_temp_symbol(rhs, "assign", dest, mode); replacement_expr_opt = rhs; } - exprt new_lhs = skip_typecast(to_binary_expr(expr).op0()); + exprt new_lhs = skip_typecast(binary_expr.op0()); rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type()); rhs.add_source_location() = expr.source_location(); code_assignt assignment(new_lhs, rhs); @@ -196,14 +190,6 @@ void goto_convertt::remove_pre( statement == ID_preincrement || statement == ID_predecrement, "expects preincrement or predecrement"); - exprt rhs; - rhs.add_source_location()=expr.source_location(); - - if(statement==ID_preincrement) - rhs.id(ID_plus); - else - rhs.id(ID_minus); - const auto &op = to_unary_expr(expr).op(); const typet &op_type = op.type(); @@ -233,8 +219,9 @@ void goto_convertt::remove_pre( else constant = from_integer(1, constant_type); - rhs.add_to_operands(op, std::move(constant)); - rhs.type() = op.type(); + exprt rhs = binary_exprt{ + op, statement == ID_preincrement ? ID_plus : ID_minus, std::move(constant)}; + rhs.add_source_location() = expr.source_location(); const bool cannot_use_lhs = result_is_used && !address_taken && needs_cleaning(op); @@ -282,14 +269,6 @@ void goto_convertt::remove_post( statement == ID_postincrement || statement == ID_postdecrement, "expects postincrement or postdecrement"); - exprt rhs; - rhs.add_source_location()=expr.source_location(); - - if(statement==ID_postincrement) - rhs.id(ID_plus); - else - rhs.id(ID_minus); - const auto &op = to_unary_expr(expr).op(); const typet &op_type = op.type(); @@ -319,8 +298,11 @@ void goto_convertt::remove_post( else constant = from_integer(1, constant_type); - rhs.add_to_operands(op, std::move(constant)); - rhs.type() = op.type(); + binary_exprt rhs{ + op, + statement == ID_postincrement ? ID_plus : ID_minus, + std::move(constant)}; + rhs.add_source_location() = expr.source_location(); code_assignt assignment(op, rhs); assignment.add_source_location()=expr.find_source_location(); diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp index 20e44a9a44e..1e9f66c945c 100644 --- a/src/jsil/jsil_convert.cpp +++ b/src/jsil/jsil_convert.cpp @@ -93,7 +93,7 @@ bool jsil_convertt::convert_code(const symbolt &symbol, codet &code) code_try_catcht t_c(std::move(t)); // Adding empty symbol to catch decl code_frontend_declt d(symbol_exprt::typeless("decl_symbol")); - t_c.add_catch(d, g); + t_c.add_catch(std::move(d), std::move(g)); t_c.add_source_location()=code.source_location(); code.swap(t_c); diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 19fe12dd050..0eabf7a4b24 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -356,7 +356,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const it++) { exprt index=from_integer(it->first, size.type()); - result.copy_to_operands(index, it->second); + result.add_to_operands(std::move(index), exprt{it->second}); } } else diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 925f4446fb9..7c110207fb7 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -1408,7 +1408,7 @@ static exprt lower_byte_update_byte_array_vector( { const exprt &element = value_as_byte_array.operands()[i]; - const exprt where = simplify_expr( + exprt where = simplify_expr( plus_exprt{src.offset(), from_integer(i, src.offset().type())}, ns); // skip elements that wouldn't change (skip over typecasts as we might have @@ -1437,9 +1437,9 @@ static exprt lower_byte_update_byte_array_vector( update_value = typecast_exprt::conditional_cast(element, subtype); if(result.id() != ID_with) - result = with_exprt{result, where, update_value}; + result = with_exprt{result, std::move(where), std::move(update_value)}; else - result.add_to_operands(where, update_value); + result.add_to_operands(std::move(where), std::move(update_value)); } return simplify_expr(std::move(result), ns); diff --git a/src/util/expr.h b/src/util/expr.h index 61b7a1caedb..150b2032422 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_EXPR_H #include "as_const.h" +#include "deprecate.h" #include "type.h" #include "validate_expressions.h" #include "validate_types.h" @@ -148,6 +149,7 @@ class exprt:public irept /// Copy the given arguments to the end of `exprt`'s operands. /// \param e1: first `exprt` to append to the operands /// \param e2: second `exprt` to append to the operands + DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&) instead")) void copy_to_operands(const exprt &e1, const exprt &e2) { operandst &op = operands(); @@ -161,6 +163,7 @@ class exprt:public irept /// Add the given arguments to the end of `exprt`'s operands. /// \param e1: first `exprt` to append to the operands /// \param e2: second `exprt` to append to the operands + DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&) instead")) void add_to_operands(const exprt &e1, const exprt &e2) { copy_to_operands(e1, e2); @@ -183,6 +186,7 @@ class exprt:public irept /// \param e1: first `exprt` to append to the operands /// \param e2: second `exprt` to append to the operands /// \param e3: third `exprt` to append to the operands + DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&, &&) instead")) void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3) { copy_to_operands(e1, e2, e3); @@ -192,6 +196,7 @@ class exprt:public irept /// \param e1: first `exprt` to append to the operands /// \param e2: second `exprt` to append to the operands /// \param e3: third `exprt` to append to the operands + DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&, &&) instead")) void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3) { operandst &op = operands(); diff --git a/src/util/std_code.h b/src/util/std_code.h index ec1030c6749..3d1d17c7b32 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -2025,9 +2025,9 @@ class code_try_catcht:public codet return to_code(operands()[2*i+2]); } - void add_catch(const code_frontend_declt &to_catch, const codet &code_catch) + void add_catch(code_frontend_declt &&to_catch, codet &&code_catch) { - add_to_operands(to_catch, code_catch); + add_to_operands(std::move(to_catch), std::move(code_catch)); } protected: