@@ -431,17 +431,17 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
431431 (to_array_type (full_type).size ().is_zero () ||
432432 to_array_type (full_type).size ().is_nil ()))
433433 {
434- // we are willing to grow an incomplete or zero-sized array
435- const auto zero = zero_initializer (
436- to_array_type (full_type).element_type (),
437- value.source_location (),
438- *this );
434+ const typet &element_type = to_array_type (full_type).element_type ();
435+
436+ // we are willing to grow an incomplete or zero-sized array --
437+ // do_initializer_list will fix up the resulting type
438+ const auto zero =
439+ zero_initializer (element_type, value.source_location (), *this );
439440 if (!zero.has_value ())
440441 {
441442 error ().source_location = value.source_location ();
442443 error () << " cannot zero-initialize array with element type '"
443- << to_string (to_type_with_subtype (full_type).subtype ())
444- << " '" << eom;
444+ << to_string (element_type) << " '" << eom;
445445 throw 0 ;
446446 }
447447 dest->operands ().resize (
@@ -978,7 +978,7 @@ exprt c_typecheck_baset::do_initializer_list(
978978 if (to_array_type (full_type).size ().is_nil ())
979979 {
980980 // start with empty array
981- result= exprt (ID_array, full_type);
981+ result = array_exprt ({}, to_array_type ( full_type) );
982982 result.add_source_location ()=value.source_location ();
983983 }
984984 else
@@ -1036,9 +1036,9 @@ exprt c_typecheck_baset::do_initializer_list(
10361036 to_array_type (full_type).size ().is_nil ())
10371037 {
10381038 // make complete by setting array size
1039- size_t size= result.operands (). size ( );
1040- result. type (). id (ID_array);
1041- result.type ().set (ID_size, from_integer (size, c_index_type () ));
1039+ array_typet &array_type = to_array_type ( result.type () );
1040+ array_type. size () =
1041+ from_integer ( result.operands ().size (), array_type. index_type ( ));
10421042 }
10431043
10441044 return result;
0 commit comments