Skip to content

Commit a4a337a

Browse files
committed
Fix union initialization
The attached test shows that we could reach recursive initialisation of unions with a byte_update instead of a union expression. The test was constructed using creduce, starting from code included in the Linux kernel.
1 parent 8cfcfdb commit a4a337a

File tree

3 files changed

+60
-16
lines changed

3 files changed

+60
-16
lines changed
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
union {
2+
int a;
3+
struct
4+
{
5+
unsigned b : 4;
6+
unsigned c : 4;
7+
};
8+
} u1 = {.b = 5, .c = 1};
9+
10+
#ifndef _MSC_VER
11+
union {
12+
int;
13+
struct
14+
{
15+
unsigned b : 4;
16+
unsigned c : 4;
17+
};
18+
} u2 = {.b = 5, .c = 1};
19+
#endif
20+
21+
int main()
22+
{
23+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
Invariant check failed
8+
--
9+
This test previously failed an internal invariant:
10+
File: ../src/ansi-c/c_typecheck_initializer.cpp:517 function: do_designated_initializer
11+
Condition: dest->id() == ID_union
12+
Reason: union should be zero initialized

src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 25 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -530,27 +530,36 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
530530
// initializer; other bytes have an unspecified value (C Standard
531531
// 6.2.6.1(7)). In practice, objects of static lifetime are fully zero
532532
// initialized.
533-
const auto zero =
534-
zero_initializer(component.type(), value.source_location(), *this);
535-
if(!zero.has_value())
536-
{
537-
error().source_location = value.source_location();
538-
error() << "cannot zero-initialize union component of type '"
539-
<< to_string(component.type()) << "'" << eom;
540-
throw 0;
541-
}
542-
543533
if(current_symbol.is_static_lifetime)
544534
{
545-
byte_update_exprt byte_update{
546-
byte_update_id(), *dest, from_integer(0, index_type()), *zero};
547-
byte_update.add_source_location() = value.source_location();
548-
*dest = std::move(byte_update);
549-
dest = &(to_byte_update_expr(*dest).op2());
535+
const auto zero =
536+
zero_initializer(component.type(), value.source_location(), *this);
537+
if(!zero.has_value())
538+
{
539+
error().source_location = value.source_location();
540+
error() << "cannot zero-initialize union component of type '"
541+
<< to_string(component.type()) << "'" << eom;
542+
throw 0;
543+
}
544+
545+
union_exprt union_expr(component.get_name(), *zero, type);
546+
union_expr.add_source_location() = value.source_location();
547+
*dest = std::move(union_expr);
548+
dest = &(to_union_expr(*dest).op());
550549
}
551550
else
552551
{
553-
union_exprt union_expr(component.get_name(), *zero, type);
552+
const auto nondet = nondet_initializer(
553+
component.type(), value.source_location(), *this);
554+
if(!nondet.has_value())
555+
{
556+
error().source_location = value.source_location();
557+
error() << "cannot nondet-initialize union component of type '"
558+
<< to_string(component.type()) << "'" << eom;
559+
throw 0;
560+
}
561+
562+
union_exprt union_expr(component.get_name(), *nondet, type);
554563
union_expr.add_source_location() = value.source_location();
555564
*dest = std::move(union_expr);
556565
dest = &(to_union_expr(*dest).op());

0 commit comments

Comments
 (0)