Merge pull request #2998 from diffblue/format-type

format(type) additions

Author: Daniel Kroening

src/util/format_type.cpp

@@ -32,6 +32,26 @@ static std::ostream &format_rec(std::ostream &os, const struct_typet &src)
   return os << " }";
 }
 
+/// format a \ref union_typet
+static std::ostream &format_rec(std::ostream &os, const union_typet &src)
+{
+  os << "union"
+     << " {";
+  bool first = true;
+
+  for(const auto &c : src.components())
+  {
+    if(first)
+      first = false;
+    else
+      os << ',';
+
+    os << ' ' << format(c.type()) << ' ' << c.get_name();
+  }
+
+  return os << " }";
+}
+
 // The below generates a string in a generic syntax
 // that is inspired by C/C++/Java, and is meant for debugging
 // purposes.
@@ -51,8 +71,24 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
   }
   else if(id == ID_struct)
     return format_rec(os, to_struct_type(type));
+  else if(id == ID_union)
+    return format_rec(os, to_union_type(type));
+  else if(id == ID_union_tag)
+    return os << "union " << to_union_tag_type(type).get_identifier();
+  else if(id == ID_struct_tag)
+    return os << "struct " << to_struct_tag_type(type).get_identifier();
+  else if(id == ID_c_enum_tag)
+    return os << "c_enum " << to_c_enum_tag_type(type).get_identifier();
   else if(id == ID_symbol_type)
     return os << "symbol_type " << to_symbol_type(type).get_identifier();
+  else if(id == ID_signedbv)
+    return os << "signedbv[" << to_signedbv_type(type).get_width() << ']';
+  else if(id == ID_unsignedbv)
+    return os << "unsignedbv[" << to_unsignedbv_type(type).get_width() << ']';
+  else if(id == ID_floatbv)
+    return os << "floatbv[" << to_floatbv_type(type).get_width() << ']';
+  else if(id == ID_c_bool)
+    return os << "c_bool[" << to_c_bool_type(type).get_width() << ']';
   else
     return os << id;
 }