Skip to content

Commit 3a24545

Browse files
committed
Partly revert "Simplify initializer to remove byte_update"
This reverts commit ac31213, which can break dump-c output: the simplified expression may have padding initialised to non-zero values. This works fine for any analysis, but breaks dump-c as padding is not included in the output. Found via tests generated CSmith, a minimised version of which is included as a regression test.
1 parent 5efb6ad commit 3a24545

File tree

4 files changed

+58
-4
lines changed

4 files changed

+58
-4
lines changed
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#include <assert.h>
2+
3+
struct S2
4+
{
5+
signed char f0;
6+
unsigned short f1;
7+
};
8+
9+
union U10 {
10+
unsigned short f0;
11+
struct S2 f3;
12+
};
13+
14+
union U10 g_2110 = {.f0 = 53747};
15+
16+
union U6 {
17+
signed f0 : 3;
18+
};
19+
20+
union U6 g_1197 = {1L};
21+
22+
int main()
23+
{
24+
assert(g_2110.f0 == 53747);
25+
26+
return 0;
27+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--dump-c
4+
VERIFICATION SUCCESSFUL
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
This test must verify successfully also for the output generated using dump-c,
11+
which previously did not correctly represent the union initializer.

src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -72,10 +72,7 @@ exprt c_typecheck_baset::do_initializer_rec(
7272
}
7373

7474
if(value.id()==ID_initializer_list)
75-
{
76-
return simplify_expr(
77-
do_initializer_list(value, type, force_constant), *this);
78-
}
75+
return do_initializer_list(value, type, force_constant);
7976

8077
if(
8178
value.id() == ID_array && value.get_bool(ID_C_string_constant) &&

src/goto-instrument/dump_c.cpp

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/byte_operators.h>
1515
#include <util/config.h>
16+
#include <util/expr_initializer.h>
1617
#include <util/find_symbols.h>
1718
#include <util/get_base_name.h>
1819
#include <util/invariant.h>
@@ -1467,6 +1468,24 @@ void dump_ct::cleanup_expr(exprt &expr)
14671468
}
14681469
}
14691470
}
1471+
else if(
1472+
ns.follow(bu.type()).id() == ID_union &&
1473+
bu.source_location().get_function().empty() &&
1474+
bu.op() == zero_initializer(bu.op().type(), source_locationt{}, ns)
1475+
.value_or(nil_exprt{}))
1476+
{
1477+
const union_typet &union_type = to_union_type(ns.follow(bu.type()));
1478+
1479+
for(const auto &comp : union_type.components())
1480+
{
1481+
if(bu.value().type() == comp.type())
1482+
{
1483+
union_exprt union_expr{comp.get_name(), bu.value(), bu.type()};
1484+
expr.swap(union_expr);
1485+
break;
1486+
}
1487+
}
1488+
}
14701489
}
14711490
}
14721491

0 commit comments

Comments
 (0)