diff --git a/regression/goto-instrument/bitfield_naming/main.c b/regression/goto-instrument/bitfield_naming/main.c new file mode 100644 index 00000000000..ec69528f52f --- /dev/null +++ b/regression/goto-instrument/bitfield_naming/main.c @@ -0,0 +1,18 @@ +typedef struct { + unsigned char b11 : 1; + unsigned char b22 : 1; + unsigned char b34 : 2; + unsigned char b58 : 4; +} bf_t; + +typedef union { + unsigned char val; + bf_t bf; +} union_bf_t; + +int main(void) +{ + union_bf_t bf; + bf.bf.b11 = 1; + return 0; +} diff --git a/regression/goto-instrument/bitfield_naming/test.desc b/regression/goto-instrument/bitfield_naming/test.desc new file mode 100644 index 00000000000..01f5b265235 --- /dev/null +++ b/regression/goto-instrument/bitfield_naming/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--show-goto-functions --json-ui +^EXIT=0$ +^SIGNAL=0$ +BF1\{U8\}\$U8\$\'b11\' +BF1\{U8\}\$U8\$\'b22\' +BF2\{U8\}\$U8\$\'b34\' +BF4\{U8\}\$U8\$\'b58\' +-- +-- + +Checks that type2name generates the right names for structs containing bitfields, +in particular including the width of bitfield fields. + diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index e9a564d35b2..4f50ba818a6 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include +#include #include "type2name.h" @@ -81,6 +83,15 @@ static std::string type2name_symbol( return result; } +static std::string pointer_offset_bits_as_string( + const typet &type, + const namespacet &ns) +{ + mp_integer bits = pointer_offset_bits(type, ns); + CHECK_RETURN(bits != -1); + return integer2string(bits); +} + static bool parent_is_sym_check=false; static std::string type2name( const typet &type, @@ -115,9 +126,9 @@ static std::string type2name( else if(type.id()==ID_empty) result+='V'; else if(type.id()==ID_signedbv) - result+="S" + type.get_string(ID_width); + result+="S" + pointer_offset_bits_as_string(type, ns); else if(type.id()==ID_unsignedbv) - result+="U" + type.get_string(ID_width); + result+="U" + pointer_offset_bits_as_string(type, ns); else if(type.id()==ID_bool || type.id()==ID_c_bool) result+='B'; @@ -128,13 +139,13 @@ static std::string type2name( else if(type.id()==ID_complex) result+='C'; else if(type.id()==ID_floatbv) - result+="F" + type.get_string(ID_width); + result+="F" + pointer_offset_bits_as_string(type, ns); else if(type.id()==ID_fixedbv) - result+="X" + type.get_string(ID_width); + result+="X" + pointer_offset_bits_as_string(type, ns); else if(type.id()==ID_natural) result+='N'; else if(type.id()==ID_pointer) - result+='*'; + result+="*" + pointer_offset_bits_as_string(type, ns); else if(type.id()==ID_reference) result+='&'; else if(type.id()==ID_code) @@ -168,7 +179,7 @@ static std::string type2name( const array_typet &t=to_array_type(type); mp_integer size; if(t.size().id()==ID_symbol) - result+="ARR"+t.size().get_string(ID_identifier); + result+="ARR"+id2string(t.size().get(ID_identifier)); else if(to_integer(t.size(), size)) result+="ARR?"; else @@ -202,7 +213,9 @@ static std::string type2name( if(it!=components.begin()) result+='|'; result+=type2name(it->type(), ns, symbol_number); - result+="'"+it->get_string(ID_name)+"'"; + irep_idt component_name = it->get_name(); + CHECK_RETURN(!component_name.empty()); + result+="'"+id2string(component_name)+"'"; } result+=']'; } @@ -230,7 +243,7 @@ static std::string type2name( else if(type.id()==ID_incomplete_c_enum) result +="EN?"; else if(type.id()==ID_c_bit_field) - result+="BF"+type.get_string(ID_size); + result+="BF"+pointer_offset_bits_as_string(type, ns); else if(type.id()==ID_vector) result+="VEC"+type.get_string(ID_size); else