Rename enum/struct/union tags in the same way as symbol

 types

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6387 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/util/rename_symbol.cpp

@@ -237,6 +237,19 @@ bool rename_symbolt::rename(typet &dest) const
       result=false;
     }
   }
+  else if(dest.id()==ID_c_enum_tag ||
+          dest.id()==ID_struct_tag ||
+          dest.id()==ID_union_tag)
+  {
+    type_mapt::const_iterator it=
+      type_map.find(to_tag_type(dest).get_identifier());
+
+    if(it!=type_map.end())
+    {
+      to_tag_type(dest).set_identifier(it->second);
+      result=false;
+    }
+  }
   else if(dest.id()==ID_array)
   {
     array_typet &array_type=to_array_type(dest);
@@ -307,6 +320,10 @@ bool rename_symbolt::have_to_rename(const typet &dest) const
   }
   else if(dest.id()==ID_symbol)
     return type_map.find(dest.get(ID_identifier))!=type_map.end();
+  else if(dest.id()==ID_c_enum_tag ||
+          dest.id()==ID_struct_tag ||
+          dest.id()==ID_union_tag)
+    return type_map.find(to_tag_type(dest).get_identifier())!=type_map.end();
   else if(dest.id()==ID_array)
     return have_to_rename(to_array_type(dest).size());
 

src/util/std_types.h

@@ -481,6 +481,35 @@ class tag_typet:public typet
   }  
 };
 
+/*! \brief Cast a generic typet to a \ref tag_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * tag_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref tag_typet
+ *
+ * \ingroup gr_std_types
+*/
+extern inline const tag_typet &to_tag_type(const typet &type)
+{
+  assert(type.id()==ID_c_enum_tag ||
+         type.id()==ID_struct_tag ||
+         type.id()==ID_union_tag);
+  return static_cast<const tag_typet &>(type);
+}
+
+/*! \copydoc to_tag_type(const typet &)
+ * \ingroup gr_std_types
+*/
+extern inline tag_typet &to_tag_type(typet &type)
+{
+  assert(type.id()==ID_c_enum_tag ||
+         type.id()==ID_struct_tag ||
+         type.id()==ID_union_tag);
+  return static_cast<tag_typet &>(type);
+}
+
 /*! \brief A struct tag type
 */