Merge pull request diffblue#1736 from hannes-steffenhagen-diffblue/develop_fix-bitfield-pretty-printing

Fix bitfield pretty printing

Author: tautschnig

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;
+}

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.
+

src/ansi-c/type2name.cpp

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/namespace.h>
 #include <util/symbol.h>
 #include <util/symbol_table.h>
+#include <util/pointer_offset_size.h>
+#include <util/invariant.h>
 
 typedef std::unordered_map<irep_idt, std::pair<size_t, bool>, 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_size);
+    result+="BF"+pointer_offset_bits_as_string(type, ns);
   else if(type.id()==ID_vector)
     result+="VEC"+type.get_string(ID_size);
   else