fx

kroening · kroening · commit dbc4f1dd7368 · 2018-05-19T12:14:52.000+01:00
diff --git a/src/analyses/invariant_propagation.cpp b/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)
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/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
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
@@ -46,8 +46,8 @@ std::string cpp_typecheckt::template_suffix(
     if(expr.id()==ID_type)
     {
       const typet &type=expr.type();
-      if(type.id()==ID_symbol)
-        result+=type.get_string(ID_identifier);
+      if(type.id()==ID_symbol_type)
+        result+=id2string(to_symbol_type(type).get_identifier());
       else
         result+=cpp_type2name(type);
     }
@@ -186,7 +186,7 @@ const symbolt &cpp_typecheckt::class_template_symbol(
 void cpp_typecheckt::elaborate_class_template(
   const typet &type)
 {
-  if(type.id()!=ID_symbol)
+  if(type.id()!=ID_symbol_type)
     return;
 
   const symbolt &symbol = lookup(to_symbol_type(type));
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
@@ -170,9 +170,9 @@ void cpp_typecheck_resolvet::remove_duplicates(
     irep_idt id;
 
     if(it->id()==ID_symbol)
-      id=it->get(ID_identifier);
-    else if(it->id()==ID_type && it->type().id()==ID_symbol)
-      id=it->type().get(ID_identifier);
+      id=to_symbol_expr(*it).get_identifier();
+    else if(it->id()==ID_type && it->type().id()==ID_symbol_type)
+      id=to_symbol_type(it->type()).get_identifier();
 
     if(id=="")
     {
@@ -350,7 +350,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
       typet followed_type=symbol.type;
       bool constant=followed_type.get_bool(ID_C_constant);
 
-      while(followed_type.id()==ID_symbol)
+      while(followed_type.id()==ID_symbol_type)
       {
         followed_type =
           cpp_typecheck.follow(to_symbol_type(followed_type));
@@ -2238,8 +2238,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
         assert(pcomp.get_bool(ID_is_type));
         const typet &type=pcomp.type();
         assert(type.id()!=ID_struct);
-        if(type.id()==ID_symbol)
-          identifier=type.get(ID_identifier);
+        if(type.id()==ID_symbol_type)
+          identifier=to_symbol_type(type).get_identifier();
         else
           continue;
       }
@@ -2260,8 +2260,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
           new_set.insert(&class_id);
           break;
         }
-        else if(symbol.type.id()==ID_symbol)
-          identifier=symbol.type.get(ID_identifier);
+        else if(symbol.type.id()==ID_symbol_type)
+          identifier=to_symbol_type(symbol.type).get_identifier();
         else
           break;
       }
@@ -2303,7 +2303,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
       if(e.id()!=ID_type)
         continue; // expressions are definitively not a scope
 
-      if(e.type().id()==ID_symbol)
+      if(e.type().id()==ID_symbol_type)
       {
         symbol_typet type=to_symbol_type(e.type());
 
@@ -2314,7 +2314,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
           const symbolt &symbol=cpp_typecheck.lookup(identifier);
           assert(symbol.is_type);
 
-          if(symbol.type.id()==ID_symbol)
+          if(symbol.type.id()==ID_symbol_type)
             type=to_symbol_type(symbol.type);
           else if(symbol.type.id()==ID_struct ||
                   symbol.type.id()==ID_incomplete_struct ||
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
@@ -793,8 +793,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
     // is it a type or not?
     if(declaration.get_bool(ID_is_type))
     {
-      parameter=exprt(ID_type, typet(ID_symbol));
-      parameter.type().set(ID_identifier, identifier);
+      parameter=exprt(ID_type, symbol_typet(identifier));
       parameter.type().add_source_location()=declaration.find_source_location();
     }
     else
@@ -829,8 +828,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
 
     if(cpp_declarator_converter.is_typedef)
     {
-      parameter=exprt(ID_type, typet(ID_symbol));
-      parameter.type().set(ID_identifier, symbol.name);
+      parameter=exprt(ID_type, symbol_typet(symbol.name));
       parameter.type().add_source_location()=declaration.find_location();
     }
     else
diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <ostream>
 
 #include <util/invariant.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 
 void template_mapt::apply(typet &type) const
 {
@@ -37,10 +39,10 @@ void template_mapt::apply(typet &type) const
       apply(subtype);
     }
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
   {
     type_mapt::const_iterator m_it=
-      type_map.find(type.get(ID_identifier));
+      type_map.find(to_symbol_type(type).get_identifier());
 
     if(m_it!=type_map.end())
     {
@@ -74,7 +76,7 @@ void template_mapt::apply(exprt &expr) const
   if(expr.id()==ID_symbol)
   {
     expr_mapt::const_iterator m_it=
-      expr_map.find(expr.get(ID_identifier));
+      expr_map.find(to_symbol_expr(expr).get_identifier());
 
     if(m_it!=expr_map.end())
     {
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
@@ -61,7 +61,7 @@ void dump_ct::operator()(std::ostream &os)
     {
       typet &type=it2->type();
 
-      if(type.id()==ID_symbol &&
+      if(type.id()==ID_symbol_type &&
          type.get_bool(ID_C_transparent_union))
       {
         symbolt new_type_sym=
@@ -314,7 +314,7 @@ void dump_ct::convert_compound(
   bool recursive,
   std::ostream &os)
 {
-  if(type.id()==ID_symbol)
+  if(type.id()==ID_symbol_type)
   {
     const symbolt &symbol=
       ns.lookup(to_symbol_type(type).get_identifier());
@@ -382,7 +382,7 @@ void dump_ct::convert_compound(
     UNREACHABLE;
     /*
     assert(parent_it->id() == ID_base);
-    assert(parent_it->get(ID_type) == ID_symbol);
+    assert(parent_it->get(ID_type) == ID_symbol_type);
 
     const irep_idt &base_id=
       parent_it->find(ID_type).get(ID_identifier);
@@ -669,7 +669,7 @@ void dump_ct::collect_typedefs_rec(
   {
     collect_typedefs_rec(type.subtype(), early, local_deps);
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
   {
     const symbolt &symbol=
       ns.lookup(to_symbol_type(type).get_identifier());
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -1429,7 +1429,7 @@ goto_programt::const_targett goto_program2codet::convert_catch(
 
 void goto_program2codet::add_local_types(const typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id()==ID_symbol_type)
   {
     const typet &full_type=ns.follow(type);
 
@@ -1662,7 +1662,7 @@ void goto_program2codet::remove_const(typet &type)
   if(type.get_bool(ID_C_constant))
     type.remove(ID_C_constant);
 
-  if(type.id()==ID_symbol)
+  if(type.id()==ID_symbol_type)
   {
     const irep_idt &identifier=to_symbol_type(type).get_identifier();
     if(!const_removed.insert(identifier).second)
@@ -1864,7 +1864,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     if(no_typecast)
       return;
 
-    assert(expr.type().id()==ID_symbol);
+    assert(expr.type().id()==ID_symbol_type);
 
     const typet &t=expr.type();
 
diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp
@@ -19,7 +19,7 @@ code_function_callt get_destructor(
   const namespacet &ns,
   const typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id()==ID_symbol_type)
   {
     return get_destructor(ns, ns.follow(type));
   }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -1039,10 +1039,11 @@ mp_integer interpretert::get_size(const typet &type)
     }
     return subtype_size;
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
   {
     return get_size(ns.follow(type));
   }
+
   return 1;
 }
 
diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h
@@ -52,7 +52,7 @@ class string_abstractiont:public messaget
 
   bool is_char_type(const typet &type) const
   {
-    if(type.id()==ID_symbol)
+    if(type.id()==ID_symbol_type)
       return is_char_type(ns.follow(type));
 
     if(type.id()!=ID_signedbv &&
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -755,7 +755,7 @@ void goto_symex_statet::rename_address(
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
-      if(member_expr.struct_op().type().id()!=ID_symbol)
+      if(member_expr.struct_op().type().id()!=ID_symbol_type)
       {
         const struct_union_typet &su_type=
           to_struct_union_type(member_expr.struct_op().type());
@@ -838,7 +838,7 @@ void goto_symex_statet::rename(
   {
     rename(type.subtype(), irep_idt(), ns, level);
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id()==ID_symbol_type)
   {
     const symbolt &symbol=
       ns.lookup(to_symbol_type(type).get_identifier());
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
@@ -44,7 +44,7 @@ static const typet &follow_tags_symbols(
   const namespacet &ns,
   const typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id()==ID_symbol_type)
     return ns.follow(type);
   else if(type.id()==ID_c_enum_tag)
     return ns.follow_tag(to_c_enum_tag_type(type));
@@ -779,7 +779,7 @@ bool linkingt::adjust_object_type_rec(
   if(base_type_eq(t1, t2, ns))
     return false;
 
-  if(t1.id()==ID_symbol ||
+  if(t1.id()==ID_symbol_type ||
      t1.id()==ID_struct_tag ||
      t1.id()==ID_union_tag ||
      t1.id()==ID_c_enum_tag)
@@ -797,7 +797,7 @@ bool linkingt::adjust_object_type_rec(
 
     return false;
   }
-  else if(t2.id()==ID_symbol ||
+  else if(t2.id()==ID_symbol_type ||
           t2.id()==ID_struct_tag ||
           t2.id()==ID_union_tag ||
           t2.id()==ID_c_enum_tag)
diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp
@@ -262,7 +262,7 @@ exprt zero_initializert::zero_initializer_rec(
 
     return value;
   }
-  else if(type_id==ID_symbol)
+  else if(type_id==ID_symbol_type)
   {
     exprt result=zero_initializer_rec(ns.follow(type), source_location);
     // we might have mangled the type for arrays, so keep that
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
@@ -36,7 +36,7 @@ bool is_char_type(const typet &type)
 
 bool is_char_array_type(const typet &type, const namespacet &ns)
 {
-  if(type.id() == ID_symbol)
+  if(type.id() == ID_symbol_type)
     return is_char_array_type(ns.follow(type), ns);
   return type.id() == ID_array && is_char_type(type.subtype());
 }
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
@@ -53,7 +53,7 @@ class base_type_eqt
 void base_type_rec(
   typet &type, const namespacet &ns, std::set<irep_idt> &symb)
 {
-  if(type.id()==ID_symbol ||
+  if(type.id()==ID_symbol_type ||
      type.id()==ID_c_enum_tag ||
      type.id()==ID_struct_tag ||
      type.id()==ID_union_tag)
@@ -87,7 +87,7 @@ void base_type_rec(
     typet &subtype=to_pointer_type(type).subtype();
 
     // we need to avoid running into an infinite loop
-    if(subtype.id()==ID_symbol ||
+    if(subtype.id()==ID_symbol_type ||
        subtype.id()==ID_c_enum_tag ||
        subtype.id()==ID_struct_tag ||
        subtype.id()==ID_union_tag)
@@ -135,7 +135,7 @@ bool base_type_eqt::base_type_eq_rec(
   #endif
 
   // loop avoidance
-  if((type1.id()==ID_symbol ||
+  if((type1.id()==ID_symbol_type ||
       type1.id()==ID_c_enum_tag ||
       type1.id()==ID_struct_tag ||
       type1.id()==ID_union_tag) &&
@@ -148,7 +148,7 @@ bool base_type_eqt::base_type_eq_rec(
       return true;
   }
 
-  if(type1.id()==ID_symbol ||
+  if(type1.id()==ID_symbol_type ||
      type1.id()==ID_c_enum_tag ||
      type1.id()==ID_struct_tag ||
      type1.id()==ID_union_tag)
@@ -162,7 +162,7 @@ bool base_type_eqt::base_type_eq_rec(
     return base_type_eq_rec(symbol.type, type2);
   }
 
-  if(type2.id()==ID_symbol ||
+  if(type2.id()==ID_symbol_type ||
      type2.id()==ID_c_enum_tag ||
      type2.id()==ID_struct_tag ||
      type2.id()==ID_union_tag)
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
@@ -51,7 +51,7 @@ void endianness_mapt::build_little_endian(const typet &src)
 
 void endianness_mapt::build_big_endian(const typet &src)
 {
-  if(src.id()==ID_symbol)
+  if(src.id()==ID_symbol_type)
     build_big_endian(ns.follow(src));
   else if(src.id()==ID_c_enum_tag)
     build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
@@ -160,8 +160,8 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
       //  dest.insert(identifier);
     }
   }
-  else if(src.id()==ID_symbol)
-    dest.insert(src.get(ID_identifier));
+  else if(src.id()==ID_symbol_type)
+    dest.insert(to_symbol_type(src).get_identifier());
   else if(src.id()==ID_array)
   {
     // do the size -- the subtype is already done
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
@@ -51,7 +51,7 @@ 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_symbol)
+  else if(id == ID_symbol_type)
     return os << "symbol_type " << to_symbol_type(type).get_identifier();
   else
     return os << id;
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
@@ -117,7 +117,7 @@ json_objectt json(
   const namespacet &ns,
   const irep_idt &mode)
 {
-  if(type.id()==ID_symbol)
+  if(type.id()==ID_symbol_type)
     return json(ns.follow(type), ns, mode);
 
   json_objectt result;
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
diff --git a/src/util/type.cpp b/src/util/type.cpp
diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp
diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp

Original file line number	Diff line number	Diff line change
`@@ -19,11 +19,10 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)`
`19`	`19`	`{`
`20`	`20`	`PRECONDITION(type.id()==ID_pointer);`
`21`	`21`
`22`		`- if(type.subtype().id()==ID_symbol)`
`23`		`- {`
	`22`	`+ if(type.subtype().id()==ID_symbol_type)`
`24`	`23`	`return to_symbol_type(type.subtype()).get_identifier();`
`25`		`- }`
`26`		`- return ID_empty;`
	`24`	`+ else`
	`25`	`+ return ID_empty;`
`27`	`26`	`}`
`28`	`27`
`29`	`28`	`/// Returns the symbol corresponding to an exception`
Original file line number	Diff line number	Diff line change
`@@ -46,8 +46,8 @@ std::string cpp_typecheckt::template_suffix(`
`46`	`46`	`if(expr.id()==ID_type)`
`47`	`47`	`{`
`48`	`48`	`const typet &type=expr.type();`
`49`		`- if(type.id()==ID_symbol)`
`50`		`- result+=type.get_string(ID_identifier);`
	`49`	`+ if(type.id()==ID_symbol_type)`
	`50`	`+ result+=id2string(to_symbol_type(type).get_identifier());`
`51`	`51`	`else`
`52`	`52`	`result+=cpp_type2name(type);`
`53`	`53`	`}`
`@@ -186,7 +186,7 @@ const symbolt &cpp_typecheckt::class_template_symbol(`
`186`	`186`	`void cpp_typecheckt::elaborate_class_template(`
`187`	`187`	`const typet &type)`
`188`	`188`	`{`
`189`		`- if(type.id()!=ID_symbol)`
	`189`	`+ if(type.id()!=ID_symbol_type)`
`190`	`190`	`return;`
`191`	`191`
`192`	`192`	`const symbolt &symbol = lookup(to_symbol_type(type));`
Original file line number	Diff line number	Diff line change
`@@ -793,8 +793,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(`
`793`	`793`	`// is it a type or not?`
`794`	`794`	`if(declaration.get_bool(ID_is_type))`
`795`	`795`	`{`
`796`		`- parameter=exprt(ID_type, typet(ID_symbol));`
`797`		`- parameter.type().set(ID_identifier, identifier);`
	`796`	`+ parameter=exprt(ID_type, symbol_typet(identifier));`
`798`	`797`	`parameter.type().add_source_location()=declaration.find_source_location();`
`799`	`798`	`}`
`800`	`799`	`else`
`@@ -829,8 +828,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(`
`829`	`828`
`830`	`829`	`if(cpp_declarator_converter.is_typedef)`
`831`	`830`	`{`
`832`		`- parameter=exprt(ID_type, typet(ID_symbol));`
`833`		`- parameter.type().set(ID_identifier, symbol.name);`
	`831`	`+ parameter=exprt(ID_type, symbol_typet(symbol.name));`
`834`	`832`	`parameter.type().add_source_location()=declaration.find_location();`
`835`	`833`	`}`
`836`	`834`	`else`
Original file line number	Diff line number	Diff line change
`@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]`
`14`	`14`	`#include <ostream>`
`15`	`15`
`16`	`16`	`#include <util/invariant.h>`
	`17`	`+#include <util/std_expr.h>`
	`18`	`+#include <util/std_types.h>`
`17`	`19`
`18`	`20`	`void template_mapt::apply(typet &type) const`
`19`	`21`	`{`
`@@ -37,10 +39,10 @@ void template_mapt::apply(typet &type) const`
`37`	`39`	`apply(subtype);`
`38`	`40`	`}`
`39`	`41`	`}`
`40`		`- else if(type.id()==ID_symbol)`
	`42`	`+ else if(type.id()==ID_symbol_type)`
`41`	`43`	`{`
`42`	`44`	`type_mapt::const_iterator m_it=`
`43`		`- type_map.find(type.get(ID_identifier));`
	`45`	`+ type_map.find(to_symbol_type(type).get_identifier());`
`44`	`46`
`45`	`47`	`if(m_it!=type_map.end())`
`46`	`48`	`{`
`@@ -74,7 +76,7 @@ void template_mapt::apply(exprt &expr) const`
`74`	`76`	`if(expr.id()==ID_symbol)`
`75`	`77`	`{`
`76`	`78`	`expr_mapt::const_iterator m_it=`
`77`		`- expr_map.find(expr.get(ID_identifier));`
	`79`	`+ expr_map.find(to_symbol_expr(expr).get_identifier());`
`78`	`80`
`79`	`81`	`if(m_it!=expr_map.end())`
`80`	`82`	`{`
Original file line number	Diff line number	Diff line change
`@@ -61,7 +61,7 @@ void dump_ct::operator()(std::ostream &os)`
`61`	`61`	`{`
`62`	`62`	`typet &type=it2->type();`
`63`	`63`
`64`		`- if(type.id()==ID_symbol &&`
	`64`	`+ if(type.id()==ID_symbol_type &&`
`65`	`65`	`type.get_bool(ID_C_transparent_union))`
`66`	`66`	`{`
`67`	`67`	`symbolt new_type_sym=`
`@@ -314,7 +314,7 @@ void dump_ct::convert_compound(`
`314`	`314`	`bool recursive,`
`315`	`315`	`std::ostream &os)`
`316`	`316`	`{`
`317`		`- if(type.id()==ID_symbol)`
	`317`	`+ if(type.id()==ID_symbol_type)`
`318`	`318`	`{`
`319`	`319`	`const symbolt &symbol=`
`320`	`320`	`ns.lookup(to_symbol_type(type).get_identifier());`
`@@ -382,7 +382,7 @@ void dump_ct::convert_compound(`
`382`	`382`	`UNREACHABLE;`
`383`	`383`	`/*`
`384`	`384`	`assert(parent_it->id() == ID_base);`
`385`		`- assert(parent_it->get(ID_type) == ID_symbol);`
	`385`	`+ assert(parent_it->get(ID_type) == ID_symbol_type);`
`386`	`386`
`387`	`387`	`const irep_idt &base_id=`
`388`	`388`	`parent_it->find(ID_type).get(ID_identifier);`
`@@ -669,7 +669,7 @@ void dump_ct::collect_typedefs_rec(`
`669`	`669`	`{`
`670`	`670`	`collect_typedefs_rec(type.subtype(), early, local_deps);`
`671`	`671`	`}`
`672`		`- else if(type.id()==ID_symbol)`
	`672`	`+ else if(type.id()==ID_symbol_type)`
`673`	`673`	`{`
`674`	`674`	`const symbolt &symbol=`
`675`	`675`	`ns.lookup(to_symbol_type(type).get_identifier());`
Original file line number	Diff line number	Diff line change
`@@ -1429,7 +1429,7 @@ goto_programt::const_targett goto_program2codet::convert_catch(`
`1429`	`1429`
`1430`	`1430`	`void goto_program2codet::add_local_types(const typet &type)`
`1431`	`1431`	`{`
`1432`		`- if(type.id()==ID_symbol)`
	`1432`	`+ if(type.id()==ID_symbol_type)`
`1433`	`1433`	`{`
`1434`	`1434`	`const typet &full_type=ns.follow(type);`
`1435`	`1435`
`@@ -1662,7 +1662,7 @@ void goto_program2codet::remove_const(typet &type)`
`1662`	`1662`	`if(type.get_bool(ID_C_constant))`
`1663`	`1663`	`type.remove(ID_C_constant);`
`1664`	`1664`
`1665`		`- if(type.id()==ID_symbol)`
	`1665`	`+ if(type.id()==ID_symbol_type)`
`1666`	`1666`	`{`
`1667`	`1667`	`const irep_idt &identifier=to_symbol_type(type).get_identifier();`
`1668`	`1668`	`if(!const_removed.insert(identifier).second)`
`@@ -1864,7 +1864,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)`
`1864`	`1864`	`if(no_typecast)`
`1865`	`1865`	`return;`
`1866`	`1866`
`1867`		`- assert(expr.type().id()==ID_symbol);`
	`1867`	`+ assert(expr.type().id()==ID_symbol_type);`
`1868`	`1868`
`1869`	`1869`	`const typet &t=expr.type();`
`1870`	`1870`
Original file line number	Diff line number	Diff line change
`@@ -19,7 +19,7 @@ code_function_callt get_destructor(`
`19`	`19`	`const namespacet &ns,`
`20`	`20`	`const typet &type)`
`21`	`21`	`{`
`22`		`- if(type.id()==ID_symbol)`
	`22`	`+ if(type.id()==ID_symbol_type)`
`23`	`23`	`{`
`24`	`24`	`return get_destructor(ns, ns.follow(type));`
`25`	`25`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1039,10 +1039,11 @@ mp_integer interpretert::get_size(const typet &type)`
`1039`	`1039`	`}`
`1040`	`1040`	`return subtype_size;`
`1041`	`1041`	`}`
`1042`		`- else if(type.id()==ID_symbol)`
	`1042`	`+ else if(type.id()==ID_symbol_type)`
`1043`	`1043`	`{`
`1044`	`1044`	`return get_size(ns.follow(type));`
`1045`	`1045`	`}`
	`1046`	`+`
`1046`	`1047`	`return 1;`
`1047`	`1048`	`}`
`1048`	`1049`