diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp index 4c42a2ba752..130f0b4fa5e 100644 --- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp +++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp @@ -1187,13 +1187,13 @@ exprt character_refine_preprocesst::expr_of_to_chars( { array_typet array_type=to_array_type(type); const typet &char_type=array_type.subtype(); - array_exprt case1(array_type); - array_exprt case2(array_type); exprt low_surrogate=expr_of_low_surrogate(chr, char_type); - case1.copy_to_operands(low_surrogate); - case2.add_to_operands( - std::move(low_surrogate), expr_of_high_surrogate(chr, char_type)); - return if_exprt(expr_of_is_bmp_code_point(chr, type), case1, case2); + array_exprt case1({low_surrogate}, array_type); + exprt high_surrogate = expr_of_high_surrogate(chr, char_type); + array_exprt case2( + {std::move(low_surrogate), std::move(high_surrogate)}, array_type); + return if_exprt( + expr_of_is_bmp_code_point(chr, type), std::move(case1), std::move(case2)); } /// Converts function call to an assignment of an expression corresponding to diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 2e05af456f5..e40f9416b1e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1614,13 +1614,14 @@ exprt java_bytecode_parsert::get_relement_value() case '[': { - array_exprt values; u2 num_values=read_u2(); + exprt::operandst values; + values.reserve(num_values); for(std::size_t i=0; i(type.find(ID_size)); mp_integer subtype_size=get_size(type.subtype()); mp_integer count; @@ -551,7 +551,7 @@ exprt interpretert::get_value( } else if(real_type.id()==ID_array) { - array_exprt result(to_array_type(real_type)); + array_exprt result({}, to_array_type(real_type)); const exprt &size_expr=static_cast(type.find(ID_size)); // Get size of array diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 18bd37af645..1069499af76 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -97,7 +97,7 @@ static void remove_vector(exprt &expr) const typet subtype=array_type.subtype(); // do component-wise: // x+y -> vector(x[0]+y[0],x[1]+y[1],...) - array_exprt array_expr(array_type); + array_exprt array_expr({}, array_type); array_expr.operands().resize(numeric_cast_v(dimension)); for(std::size_t i=0; i vector(-x[0],-x[1],...) - array_exprt array_expr(array_type); + array_exprt array_expr({}, array_type); array_expr.operands().resize(numeric_cast_v(dimension)); for(std::size_t i=0; i(array_type.size()); exprt casted_op = typecast_exprt::conditional_cast(op, array_type.subtype()); - array_exprt array_expr(array_type); - array_expr.operands().resize(dimension, op); - expr = array_expr; + expr = array_exprt(exprt::operandst(dimension, casted_op), array_type); } } } diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index a85f97f6465..74a469e5ae0 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -36,7 +36,7 @@ static exprt unpack_rec( const namespacet &ns, bool unpack_byte_array=false) { - array_exprt array( + array_exprt array({}, array_typet(unsignedbv_typet(8), from_integer(0, size_type()))); // endianness_mapt should be the point of reference for mapping out @@ -240,7 +240,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) element_width.has_value() && *element_width >= 1 && *element_width % 8 == 0 && to_integer(array_type.size(), num_elements)) { - array_exprt array(array_type); + array_exprt array({}, array_type); for(mp_integer i=0; i add_axioms_from_float_scientific_notation( two_power_e_over_ten_power_d_table.size(), int_type); array_exprt conversion_factor_table( - array_typet(float_type, conversion_factor_table_size)); + {}, array_typet(float_type, conversion_factor_table_size)); for(const auto &negative : two_power_e_over_ten_power_d_table_negatives) conversion_factor_table.copy_to_operands( constant_float(negative, float_spec)); diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 4e76ed44559..4686bfaf2e6 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -171,7 +171,7 @@ array_exprt interval_sparse_arrayt::concretize( { const array_typet array_type( default_value.type(), from_integer(size, index_type)); - array_exprt array(array_type); + array_exprt array({}, array_type); array.operands().reserve(size); auto it = entries.begin(); diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 6402a7edf5a..0ea2c515ee1 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -122,7 +122,7 @@ exprt expr_initializert::expr_initializer_rec( { // we initialize this with an empty array - array_exprt value(array_type); + array_exprt value({}, array_type); value.type().id(ID_array); value.type().set(ID_size, from_integer(0, size_type())); value.add_source_location()=source_location; @@ -157,7 +157,7 @@ exprt expr_initializert::expr_initializer_rec( if(*array_size < 0) return nil_exprt(); - array_exprt value(array_type); + array_exprt value({}, array_type); value.operands().resize(numeric_cast_v(*array_size), tmpval); value.add_source_location()=source_location; return std::move(value); diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 72d8442b01e..06080b1599f 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1540,7 +1540,7 @@ exprt simplify_exprt::bits2expr( const std::size_t el_size = numeric_cast_v(*el_size_opt); - array_exprt result(array_type); + array_exprt result({}, array_type); result.reserve_operands(n_el); for(std::size_t i=0; i