Merge pull request #3086 from diffblue/symbol_type_fixup

bugfix: use symbol_type for type symbol

Author: Daniel Kroening

src/pointer-analysis/value_set_analysis_fi.cpp

@@ -190,7 +190,7 @@ bool value_set_analysis_fit::check_type(const typet &type)
   }
   else if(type.id()==ID_array)
     return check_type(type.subtype());
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     return check_type(ns.follow(type));
 
   return false;

src/pointer-analysis/value_set_analysis_fivr.cpp

@@ -178,7 +178,7 @@ bool value_set_analysis_fivrt::check_type(const typet &type)
   }
   else if(type.id()==ID_array)
     return check_type(type.subtype());
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     return check_type(ns.follow(type));
 
   return false;

src/pointer-analysis/value_set_analysis_fivrns.cpp

@@ -178,7 +178,7 @@ bool value_set_analysis_fivrnst::check_type(const typet &type)
     }
     else if(type.id()==ID_array)
       return check_type(type.subtype());
-    else if(type.id()==ID_symbol)
+    else if(type.id() == ID_symbol_type)
       return check_type(ns.follow(type));
 
   return false;

src/solvers/flattening/boolbv.cpp

@@ -623,7 +623,7 @@ exprt boolbvt::make_free_bv_expr(const typet &type)
 
 bool boolbvt::is_unbounded_array(const typet &type) const
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     return is_unbounded_array(ns.follow(type));
 
   if(type.id()!=ID_array)

src/solvers/flattening/boolbv_get.cpp

@@ -71,7 +71,7 @@ exprt boolbvt::bv_get_rec(
   std::size_t offset,
   const typet &type) const
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     return bv_get_rec(bv, unknown, offset, ns.follow(type));
 
   std::size_t width=boolbv_width(type);

src/solvers/flattening/boolbv_map.cpp

@@ -50,7 +50,7 @@ boolbv_mapt::map_entryt &boolbv_mapt::get_map_entry(
   const irep_idt &identifier,
   const typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     return get_map_entry(identifier, ns.follow(type));
 
   std::pair<mappingt::iterator, bool> result=

src/solvers/flattening/boolbv_update.cpp

@@ -42,7 +42,7 @@ void boolbvt::convert_update_rec(
   const exprt &new_value,
   bvt &bv)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     convert_update_rec(
       designators, d, ns.follow(type), offset, new_value, bv);
 

src/solvers/flattening/boolbv_with.cpp

@@ -100,7 +100,7 @@ void boolbvt::convert_with(
   else if(type.id() == ID_union_tag)
     return convert_with(
       ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);
 
   error().source_location=type.source_location();

src/solvers/smt2/smt2_conv.cpp

@@ -3978,7 +3978,7 @@ void smt2_convt::unflatten(
   const typet &type,
   unsigned nesting)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     return unflatten(where, ns.follow(type));
 
   if(type.id()==ID_bool)
@@ -4503,7 +4503,7 @@ void smt2_convt::convert_type(const typet &type)
     out << "Real";
   else if(type.id()==ID_integer)
     out << "Int";
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     convert_type(ns.follow(type));
   else if(type.id()==ID_complex)
   {
@@ -4722,7 +4722,7 @@ void smt2_convt::find_symbols_rec(
   {
     find_symbols_rec(type.subtype(), recstack);
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     const symbol_typet &st=to_symbol_type(type);
     const irep_idt &id=st.get_identifier();