Merge pull request #3762 from tautschnig/no-follow-goto-instrument

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

Author: tautschnig

src/goto-instrument/accelerate/overflow_instrumenter.cpp

@@ -100,7 +100,7 @@ void overflow_instrumentert::overflow_expr(
     overflow_expr(*it, cases);
   }
 
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   if(expr.id()==ID_typecast)
   {
@@ -109,7 +109,7 @@ void overflow_instrumentert::overflow_expr(
       return;
     }
 
-    const typet &old_type=ns.follow(expr.op0().type());
+    const typet &old_type = expr.op0().type();
     const std::size_t new_width = to_bitvector_type(expr.type()).get_width();
     const std::size_t old_width = to_bitvector_type(old_type).get_width();
 

src/goto-instrument/dump_c.cpp

@@ -421,9 +421,9 @@ void dump_ct::convert_compound(
        comp.get_is_padding())
       continue;
 
-    const typet *non_array_type=&ns.follow(comp_type);
+    const typet *non_array_type = &comp_type;
     while(non_array_type->id()==ID_array)
-      non_array_type=&(ns.follow(non_array_type->subtype()));
+      non_array_type = &(non_array_type->subtype());
 
     if(recursive)
     {

src/goto-instrument/goto_program2code.cpp

@@ -405,8 +405,7 @@ void goto_program2codet::convert_assign_rec(
 {
   if(assign.rhs().id()==ID_array)
   {
-    const array_typet &type=
-      to_array_type(ns.follow(assign.rhs().type()));
+    const array_typet &type = to_array_type(assign.rhs().type());
 
     unsigned i=0;
     forall_operands(it, assign.rhs())
@@ -1575,7 +1574,7 @@ void goto_program2codet::cleanup_function_call(
       code_typet::parameterst::const_iterator it=parameters.begin();
       Forall_expr(it2, arguments)
       {
-        if(ns.follow(it2->type()).id()==ID_union)
+        if(it2->type().id() == ID_union || it2->type().id() == ID_union_tag)
           it2->type()=it->type();
         ++it;
       }
@@ -1825,8 +1824,9 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
   }
 
   // work around transparent union argument
-  if(expr.id()==ID_union &&
-     ns.follow(expr.type()).id()!=ID_union)
+  if(
+    expr.id() == ID_union && expr.type().id() != ID_union &&
+    expr.type().id() != ID_union_tag)
   {
     expr=to_union_expr(expr).op();
   }
@@ -1977,7 +1977,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
   }
   else if(expr.id()==ID_typecast)
   {
-    if(ns.follow(expr.type()).id()==ID_c_bit_field)
+    if(expr.type().id() == ID_c_bit_field)
       expr=to_typecast_expr(expr).op();
     else
     {