diff --git a/regression/cbmc-cpp/Assignment_Array_Member/main.cpp b/regression/cbmc-cpp/Assignment_Array_Member/main.cpp new file mode 100644 index 000000000000..8e4bc83135ba --- /dev/null +++ b/regression/cbmc-cpp/Assignment_Array_Member/main.cpp @@ -0,0 +1,26 @@ +// Author: Wang Chuanhao +/// \file +/// Implicit copy assignment copies every element of an array member. + +#include + +struct S +{ + int values[2]; + + S() + { + values[0] = 0; + values[1] = 0; + } +}; + +int main() +{ + S source, destination; + source.values[0] = 7; + source.values[1] = 11; + destination = source; + assert(destination.values[0] == 7); + assert(destination.values[1] == 11); +} diff --git a/regression/cbmc-cpp/Assignment_Array_Member/test.desc b/regression/cbmc-cpp/Assignment_Array_Member/test.desc new file mode 100644 index 000000000000..91d9cf8b52eb --- /dev/null +++ b/regression/cbmc-cpp/Assignment_Array_Member/test.desc @@ -0,0 +1,8 @@ +CORE +main.cpp + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 79709e447a2c..93b6cec11d95 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -99,9 +99,10 @@ static void copy_array( ID_component_cpp_name, cpp_namet(member_base_name, source_location)); member.copy_to_operands(cpp_namet(arg_name, source_location).as_expr()); + // The array operands are not typechecked yet, so avoid index_exprt's checks. side_effect_expr_assignt assign( - index_exprt(array.as_expr(), constant), - index_exprt(member, constant), + binary_exprt(array.as_expr(), ID_index, constant, uninitialized_typet()), + binary_exprt(member, ID_index, constant, uninitialized_typet()), typet(), source_location); @@ -392,7 +393,7 @@ void cpp_typecheckt::default_assignop_value( } const auto size = numeric_cast(size_expr); - CHECK_RETURN(!size.has_value()); + CHECK_RETURN(size.has_value()); CHECK_RETURN(*size >= 0); for(mp_integer i = 0; i < *size; ++i)