From 651d8d1b804bae54e636907fc8bc9521da264007 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Wed, 20 Dec 2017 15:07:27 +0000 Subject: [PATCH 1/3] Fixes use of wrong identifier when pretty printing bitfield types --- src/ansi-c/type2name.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 0a49ae57e77..2cb562bf4eb 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -233,7 +233,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"+type.get_string(ID_width); else if(type.id()==ID_vector) result+="VEC"+type.get_string(ID_size); else From 82a7ec62264ed80e7e3e8457eed4037451a38b7c Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 21 Dec 2017 14:15:15 +0000 Subject: [PATCH 2/3] Adds regression test for bitfield naming bug --- .../goto-instrument/bitfield_naming/main.c | 18 ++++++++++++++++++ .../goto-instrument/bitfield_naming/test.desc | 15 +++++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 regression/goto-instrument/bitfield_naming/main.c create mode 100644 regression/goto-instrument/bitfield_naming/test.desc 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. + From 4f1a67abb4c8b2ea4024390798156d826471e3b6 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 21 Dec 2017 14:48:06 +0000 Subject: [PATCH 3/3] Uses alternatives to get_string in type2name when possible --- src/ansi-c/type2name.cpp | 27 ++++++++++++++++++++------- 1 file changed, 20 insertions(+), 7 deletions(-) diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 2cb562bf4eb..c42b63f5a15 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include +#include typedef std::unordered_map, irep_id_hash> symbol_numbert; @@ -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,9 +139,9 @@ 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) @@ -171,7 +182,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 @@ -205,7 +216,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+=']'; } @@ -233,7 +246,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_width); + result+="BF"+pointer_offset_bits_as_string(type, ns); else if(type.id()==ID_vector) result+="VEC"+type.get_string(ID_size); else