diff --git a/regression/goto-instrument/dump-union2/main.c b/regression/goto-instrument/dump-union2/main.c new file mode 100644 index 00000000000..f09a56879c4 --- /dev/null +++ b/regression/goto-instrument/dump-union2/main.c @@ -0,0 +1,27 @@ +#include + +struct S2 +{ + signed char f0; + unsigned short f1; +}; + +union U10 { + unsigned short f0; + struct S2 f3; +}; + +union U10 g_2110 = {.f0 = 53747}; + +union U6 { + signed f0 : 3; +}; + +union U6 g_1197 = {1L}; + +int main() +{ + assert(g_2110.f0 == 53747); + + return 0; +} diff --git a/regression/goto-instrument/dump-union2/test.desc b/regression/goto-instrument/dump-union2/test.desc new file mode 100644 index 00000000000..f85d80fbebd --- /dev/null +++ b/regression/goto-instrument/dump-union2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--dump-c +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test must verify successfully also for the output generated using dump-c, +which previously did not correctly represent the union initializer. diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index c8a8065a644..bf82c39bdca 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -72,10 +72,7 @@ exprt c_typecheck_baset::do_initializer_rec( } if(value.id()==ID_initializer_list) - { - return simplify_expr( - do_initializer_list(value, type, force_constant), *this); - } + return do_initializer_list(value, type, force_constant); if( value.id() == ID_array && value.get_bool(ID_C_string_constant) && diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index ada5dfeb645..3e414f61ee4 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -1467,6 +1468,24 @@ void dump_ct::cleanup_expr(exprt &expr) } } } + else if( + ns.follow(bu.type()).id() == ID_union && + bu.source_location().get_function().empty() && + bu.op() == zero_initializer(bu.op().type(), source_locationt{}, ns) + .value_or(nil_exprt{})) + { + const union_typet &union_type = to_union_type(ns.follow(bu.type())); + + for(const auto &comp : union_type.components()) + { + if(bu.value().type() == comp.type()) + { + union_exprt union_expr{comp.get_name(), bu.value(), bu.type()}; + expr.swap(union_expr); + break; + } + } + } } }