Skip to content

Commit eea3a11

Browse files
committed
C front-end: printing enum type declarations with bitvector awareness
The constants are no longer stored as string literals, and instead use the bitvector representation (currently: hexadecimal values). Also make regression tests print the dump-c generated C code in regression tests.
1 parent e23bf5c commit eea3a11

File tree

3 files changed

+34
-2
lines changed

3 files changed

+34
-2
lines changed
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
enum hex
4+
{
5+
V1 = 0x1,
6+
V10 = 0xA,
7+
V11 = 11
8+
};
9+
10+
int main()
11+
{
12+
enum hex h = V10;
13+
assert(0xca == (unsigned char)(char)0b11001010);
14+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--dump-c
4+
enum hex \{ .* \};
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
This test must pass running CBMC on the output generated using dump-c to
11+
demonstrate that the enum output wouldn't generate A and B (just those
12+
characters, no quotes or 0x prefix) instead of 10 and 11, respectively.

src/ansi-c/expr2c.cpp

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -378,21 +378,27 @@ std::string expr2ct::convert_rec(
378378

379379
if(!to_c_enum_type(src).is_incomplete())
380380
{
381+
const c_enum_typet &c_enum_type = to_c_enum_type(src);
382+
const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
383+
const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
384+
381385
result += '{';
382386

383387
// add members
384-
const c_enum_typet::memberst &members = to_c_enum_type(src).members();
388+
const c_enum_typet::memberst &members = c_enum_type.members();
385389

386390
for(c_enum_typet::memberst::const_iterator it = members.begin();
387391
it != members.end();
388392
it++)
389393
{
394+
mp_integer int_value = bvrep2integer(it->get_value(), width, is_signed);
395+
390396
if(it != members.begin())
391397
result += ',';
392398
result += ' ';
393399
result += id2string(it->get_base_name());
394400
result += '=';
395-
result += id2string(it->get_value());
401+
result += integer2string(int_value);
396402
}
397403

398404
result += " }";

0 commit comments

Comments
 (0)