Merge pull request #7589 from tautschnig/bugfixes/vector-name

C front-end: fix type2name for vectors

Author: kroening

regression/ansi-c/gcc_vector2/main.c

@@ -0,0 +1,27 @@
+typedef int __v4 __attribute__((__vector_size__(16)));
+typedef int __v8 __attribute__((__vector_size__(32)));
+typedef int __v16 __attribute__((__vector_size__(64)));
+
+__v8 foo(__v16 __A)
+{
+  union
+  {
+    __v8 __a[2];
+    __v16 __v;
+  } __u = {.__v = __A};
+  return __u.__a[0];
+}
+
+__v4 bar(__v8 __A)
+{
+  union
+  {
+    __v4 __a[2];
+    __v8 __v;
+  } __u = {.__v = __A};
+  return __u.__a[0];
+}
+
+int main()
+{
+}

regression/ansi-c/gcc_vector2/test.desc

@@ -0,0 +1,11 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+We previously got a spurious type conflict for both unions got the same tag name
+(as type2name did not correctly name vectors of different size).

regression/goto-instrument/bitfield_naming/test.desc

@@ -3,10 +3,10 @@ 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\'
+BF1\{U8\}\'b11\'
+BF1\{U8\}\'b22\'
+BF2\{U8\}\'b34\'
+BF4\{U8\}\'b58\'
 --
 --
 

src/ansi-c/type2name.cpp

@@ -245,7 +245,11 @@ static std::string type2name(
   else if(type.id()==ID_c_bit_field)
     result+="BF"+pointer_offset_bits_as_string(type, ns);
   else if(type.id()==ID_vector)
-    result+="VEC"+type.get_string(ID_size);
+  {
+    const constant_exprt &size = to_vector_type(type).size();
+    const auto size_int = numeric_cast_v<mp_integer>(size);
+    result += "VEC" + integer2string(size_int);
+  }
   else
     throw "unknown type '"+type.id_string()+"' encountered";
 
@@ -256,8 +260,7 @@ static std::string type2name(
       type2name(to_type_with_subtype(type).subtype(), ns, symbol_number);
     result+='}';
   }
-
-  if(type.has_subtypes())
+  else if(type.has_subtypes())
   {
     result+='$';
     for(const typet &subtype : to_type_with_subtypes(type).subtypes())