type symbols now use ID_symbol_type

Author: Daniel Kroening

src/analyses/invariant_propagation.cpp

@@ -189,7 +189,7 @@ bool invariant_propagationt::check_type(const typet &type) const
     return false;
   else if(type.id()==ID_array)
     return false;
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
     return check_type(ns.follow(type));
   else if(type.id()==ID_unsignedbv ||
           type.id()==ID_signedbv)

src/analyses/uncaught_exceptions_analysis.cpp

@@ -19,11 +19,10 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_pointer);
 
-  if(type.subtype().id()==ID_symbol)
-  {
+  if(type.subtype().id()==ID_symbol_type)
     return to_symbol_type(type.subtype()).get_identifier();
-  }
-  return ID_empty;
+  else
+    return ID_empty;
 }
 
 /// Returns the symbol corresponding to an exception

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(to_symbol_type(result_type));
@@ -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

@@ -383,7 +383,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)
     {
@@ -3032,8 +3032,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

@@ -457,7 +457,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

@@ -187,7 +187,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)
   {