Skip to content

Commit c1a62de

Browse files
committed
to_bitvector_type must not be used on enum types
We need to resolve the tag type and look into the subtype.
1 parent 65b0939 commit c1a62de

File tree

1 file changed

+13
-4
lines changed

1 file changed

+13
-4
lines changed

src/util/simplify_expr.cpp

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1558,25 +1558,34 @@ optionalt<std::string> simplify_exprt::expr2bits(
15581558

15591559
if(expr.id()==ID_constant)
15601560
{
1561+
const auto &value = to_constant_expr(expr).get_value();
1562+
15611563
if(type.id()==ID_unsignedbv ||
15621564
type.id()==ID_signedbv ||
1563-
type.id()==ID_c_enum ||
1564-
type.id()==ID_c_enum_tag ||
15651565
type.id()==ID_floatbv ||
15661566
type.id()==ID_fixedbv)
15671567
{
15681568
const auto width = to_bitvector_type(type).get_width();
1569-
const auto &bvrep = to_constant_expr(expr).get_value();
15701569

15711570
endianness_mapt map(type, little_endian, ns);
15721571

15731572
std::string result(width, ' ');
15741573

15751574
for(std::string::size_type i = 0; i < width; ++i)
1576-
result[map.map_bit(i)] = get_bvrep_bit(bvrep, width, i) ? '1' : '0';
1575+
result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0';
15771576

15781577
return result;
15791578
}
1579+
else if(type.id() == ID_c_enum_tag)
1580+
{
1581+
const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type));
1582+
return expr2bits(constant_exprt(value, c_enum_type), little_endian);
1583+
}
1584+
else if(type.id() == ID_c_enum)
1585+
{
1586+
return expr2bits(
1587+
constant_exprt(value, to_c_enum_type(type).subtype(), little_endian);
1588+
}
15801589
}
15811590
else if(expr.id()==ID_union)
15821591
{

0 commit comments

Comments
 (0)