Merge pull request #3760 from tautschnig/no-follow-goto-symex

Remove unnecessary use of ns.follow in goto-symex/

Author: kroening

src/goto-symex/auto_objects.cpp

@@ -57,7 +57,7 @@ void goto_symext::initialize_auto_object(
   else if(type.id()==ID_pointer)
   {
     const pointer_typet &pointer_type=to_pointer_type(type);
-    const typet &subtype = ns.follow(pointer_type.subtype());
+    const typet &subtype = pointer_type.subtype();
 
     // we don't like function pointers and
     // we don't like void *

src/goto-symex/goto_symex_state.cpp

@@ -321,7 +321,7 @@ void goto_symex_statet::rename(
   else if(expr.id()==ID_symbol)
   {
     // we never rename function symbols
-    if(ns.follow(expr.type()).id()==ID_code)
+    if(expr.type().id() == ID_code)
     {
       rename(
         expr.type(),

src/goto-symex/symex_assign.cpp

@@ -307,7 +307,7 @@ void goto_symext::symex_assign_array(
 {
   const exprt &lhs_array=lhs.array();
   const exprt &lhs_index=lhs.index();
-  const typet &lhs_index_type = ns.follow(lhs_array.type());
+  const typet &lhs_index_type = lhs_array.type();
 
   PRECONDITION(lhs_index_type.id() == ID_array);
 
@@ -371,9 +371,8 @@ void goto_symext::symex_assign_struct_member(
     {
       // remove the type cast, we assume that the member is there
       exprt tmp = to_typecast_expr(lhs_struct).op();
-      const typet &op0_type=ns.follow(tmp.type());
 
-      if(op0_type.id()==ID_struct)
+      if(tmp.type().id() == ID_struct || tmp.type().id() == ID_struct_tag)
         lhs_struct=tmp;
       else
         return; // ignore and give up

src/goto-symex/symex_dead.cpp

@@ -30,7 +30,7 @@ void goto_symext::symex_dead(statet &state)
   state.rename(ssa, ns, goto_symex_statet::L1);
 
   // in case of pointers, put something into the value set
-  if(ns.follow(code.symbol().type()).id() == ID_pointer)
+  if(code.symbol().type().id() == ID_pointer)
   {
     exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns);
 

src/goto-symex/symex_decl.cpp

@@ -46,7 +46,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   ssa.update_type();
 
   // in case of pointers, put something into the value set
-  if(ns.follow(expr.type()).id()==ID_pointer)
+  if(expr.type().id() == ID_pointer)
   {
     exprt failed=
       get_failed_symbol(expr, ns);