type symbols now use ID_symbol_type

Author: Daniel Kroening

src/ansi-c/c_typecast.cpp

@@ -252,15 +252,15 @@ bool check_c_implicit_typecast(
 
 typet c_typecastt::follow_with_qualifiers(const typet &src_type)
 {
-  if(src_type.id()!=ID_symbol)
+  if(src_type.id()!=ID_symbol_type)
     return src_type;
 
   typet result_type=src_type;
 
   // collect qualifiers
   c_qualifierst qualifiers(src_type);
 
-  while(result_type.id()==ID_symbol)
+  while(result_type.id()==ID_symbol_type)
   {
     const symbolt &followed_type_symbol=
       ns.lookup(result_type.get(ID_identifier));
@@ -345,7 +345,7 @@ c_typecastt::c_typet c_typecastt::get_c_type(
   {
     return INT;
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
     return get_c_type(ns.follow(type));
   else if(type.id()==ID_rational)
     return RATIONAL;

src/ansi-c/c_typecheck_base.cpp

@@ -404,7 +404,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
        final_old.subtype()==final_new.subtype())
     {
       // we don't do symbol types for arrays anymore
-      PRECONDITION(old_symbol.type.id()!=ID_symbol);
+      PRECONDITION(old_symbol.type.id()!=ID_symbol_type);
       old_symbol.type=new_symbol.type;
     }
     else if((final_old.id()==ID_incomplete_c_enum ||

src/ansi-c/c_typecheck_code.cpp

@@ -384,7 +384,7 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
   }
   else if(type.id()==ID_vector)
     return is_complete_type(type.subtype());
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
     return is_complete_type(follow(type));
 
   return true;

src/ansi-c/c_typecheck_expr.cpp

@@ -88,9 +88,9 @@ bool c_typecheck_baset::gcc_types_compatible_p(
   // read
   // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
 
-  if(type1.id()==ID_symbol)
+  if(type1.id()==ID_symbol_type)
     return gcc_types_compatible_p(follow(type1), type2);
-  else if(type2.id()==ID_symbol)
+  else if(type2.id()==ID_symbol_type)
     return gcc_types_compatible_p(type1, follow(type2));
 
   // check qualifiers first
@@ -523,8 +523,8 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
 
   forall_operands(m_it, member)
   {
-    if(type.id()==ID_symbol)
-      type=follow(type);
+    if(type.id()==ID_symbol_type)
+      type=follow(to_symbol_type(type));
 
     if(m_it->id()==ID_member)
     {
@@ -2956,8 +2956,8 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
 
   typet subtype=type.subtype();
 
-  if(subtype.id()==ID_symbol)
-    subtype=follow(subtype);
+  if(subtype.id()==ID_symbol_type)
+    subtype=follow(to_symbol_type(subtype));
 
   if(subtype.id()==ID_incomplete_struct)
   {

src/ansi-c/expr2c.cpp

@@ -446,7 +446,7 @@ std::string expr2ct::convert_rec(
     return convert_rec(
       src.subtype(), qualifiers, declarator+"[]");
   }
-  else if(src.id()==ID_symbol)
+  else if(src.id()==ID_symbol_type)
   {
     symbol_typet symbolic_type=to_symbol_type(src);
     const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);

src/ansi-c/padding.cpp

@@ -82,8 +82,8 @@ mp_integer alignment(const typet &type, const namespacet &ns)
     result=alignment(type.subtype(), ns);
   else if(type.id()==ID_c_enum_tag)
     result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
-  else if(type.id()==ID_symbol)
-    result=alignment(ns.follow(type), ns);
+  else if(type.id()==ID_symbol_type)
+    result=alignment(ns.follow(to_symbol_type(type)), ns);
   else if(type.id()==ID_c_bit_field)
   {
     // we align these according to the 'underlying type'

src/ansi-c/type2name.cpp

@@ -186,7 +186,7 @@ static std::string type2name(
     else
       result+="ARR"+integer2string(size);
   }
-  else if(type.id()==ID_symbol ||
+  else if(type.id()==ID_symbol_type ||
           type.id()==ID_c_enum_tag ||
           type.id()==ID_struct_tag ||
           type.id()==ID_union_tag)

src/cpp/cpp_convert_type.cpp

@@ -574,7 +574,7 @@ void cpp_convert_plain_type(typet &type)
      type.id()==ID_bool ||
      type.id()==ID_floatbv ||
      type.id()==ID_empty ||
-     type.id()==ID_symbol ||
+     type.id()==ID_symbol_type ||
      type.id()==ID_constructor ||
      type.id()==ID_destructor)
   {

src/util/irep_ids.def

@@ -58,6 +58,7 @@ IREP_ID_ONE(bitxnor)
 IREP_ID_ONE(notequal)
 IREP_ID_ONE(if)
 IREP_ID_ONE(symbol)
+IREP_ID_ONE(symbol_type)
 IREP_ID_ONE(next_symbol)
 IREP_ID_ONE(nondet_symbol)
 IREP_ID_ONE(predicate_symbol)

src/util/namespace.cpp

@@ -62,7 +62,7 @@ const symbolt &namespace_baset::lookup(const tag_typet &type) const
 
 const typet &namespace_baset::follow(const typet &src) const
 {
-  if(src.id()!=ID_symbol)
+  if(src.id()!=ID_symbol_type)
     return src;
 
   const symbolt *symbol = &lookup(to_symbol_type(src));
@@ -72,7 +72,7 @@ const typet &namespace_baset::follow(const typet &src) const
   {
     DATA_INVARIANT(symbol->is_type, "symbol type points to type");
 
-    if(symbol->type.id() == ID_symbol)
+    if(symbol->type.id() == ID_symbol_type)
       symbol = &lookup(to_symbol_type(symbol->type));
     else
       return symbol->type;

src/util/std_types.h

@@ -110,11 +110,11 @@ class real_typet:public typet
 class symbol_typet:public typet
 {
 public:
-  symbol_typet():typet(ID_symbol)
+  symbol_typet():typet(ID_symbol_type)
   {
   }
 
-  explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol)
+  explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol_type)
   {
     set_identifier(identifier);
   }
@@ -142,7 +142,7 @@ class symbol_typet:public typet
 */
 inline const symbol_typet &to_symbol_type(const typet &type)
 {
-  PRECONDITION(type.id()==ID_symbol);
+  PRECONDITION(type.id()==ID_symbol_type);
   return static_cast<const symbol_typet &>(type);
 }
 
@@ -151,7 +151,7 @@ inline const symbol_typet &to_symbol_type(const typet &type)
 */
 inline symbol_typet &to_symbol_type(typet &type)
 {
-  PRECONDITION(type.id()==ID_symbol);
+  PRECONDITION(type.id()==ID_symbol_type);
   return static_cast<symbol_typet &>(type);
 }