Merge pull request #8215 from tautschnig/cleanup/no-follow-analyses

analyses: Replace uses of namespacet::follow

src/analyses/custom_bitvector_analysis.cpp

@@ -233,8 +233,10 @@ void custom_bitvector_domaint::assign_struct_rec(
 {
   if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
   {
-    const struct_typet &struct_type=
-      to_struct_type(ns.follow(lhs.type()));
+    const struct_typet &struct_type =
+      lhs.type().id() == ID_struct
+        ? to_struct_type(lhs.type())
+        : ns.follow_tag(to_struct_tag_type(lhs.type()));
 
     // assign member-by-member
     for(const auto &c : struct_type.components())

src/analyses/goto_rw.cpp

@@ -250,7 +250,9 @@ void rw_range_sett::get_objects_member(
     return;
   }
 
-  const struct_typet &struct_type = to_struct_type(ns.follow(type));
+  const struct_typet &struct_type = type.id() == ID_struct
+                                      ? to_struct_type(type)
+                                      : ns.follow_tag(to_struct_tag_type(type));
 
   auto offset_bits =
     member_offset_bits(struct_type, expr.get_component_name(), ns);
@@ -367,8 +369,10 @@ void rw_range_sett::get_objects_struct(
   const range_spect &range_start,
   const range_spect &size)
 {
-  const struct_typet &struct_type=
-    to_struct_type(ns.follow(expr.type()));
+  const struct_typet &struct_type =
+    expr.type().id() == ID_struct
+      ? to_struct_type(expr.type())
+      : ns.follow_tag(to_struct_tag_type(expr.type()));
 
   auto struct_bits = pointer_offset_bits(struct_type, ns);
 

src/analyses/invariant_propagation.cpp

@@ -131,7 +131,10 @@ void invariant_propagationt::get_objects_rec(
     t.id() == ID_struct || t.id() == ID_union || t.id() == ID_struct_tag ||
     t.id() == ID_union_tag)
   {
-    const struct_union_typet &struct_type = to_struct_union_type(ns.follow(t));
+    const struct_union_typet &struct_type =
+      (t.id() == ID_struct_tag || t.id() == ID_union_tag)
+        ? ns.follow_tag(to_struct_or_union_tag_type(t))
+        : to_struct_union_type(t);
 
     for(const auto &component : struct_type.components())
     {
@@ -223,7 +226,9 @@ bool invariant_propagationt::check_type(const typet &type) const
   else if(
     type.id() == ID_struct || type.id() == ID_union ||
     type.id() == ID_struct_tag || type.id() == ID_union_tag)
+  {
     return false;
+  }
   else if(type.id()==ID_array)
     return false;
   else if(type.id()==ID_unsignedbv ||

src/analyses/invariant_set.cpp

@@ -474,7 +474,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
 
     if(op_type.id() == ID_struct || op_type.id() == ID_struct_tag)
     {
-      const struct_typet &struct_type = to_struct_type(ns.follow(op_type));
+      const struct_typet &struct_type =
+        op_type.id() == ID_struct ? to_struct_type(op_type)
+                                  : ns.follow_tag(to_struct_tag_type(op_type));
 
       for(const auto &comp : struct_type.components())
       {

src/analyses/variable-sensitivity/abstract_aggregate_object.h

@@ -33,7 +33,13 @@ class abstract_aggregate_objectt : public abstract_objectt,
   abstract_aggregate_objectt(const typet &type, bool tp, bool bttm)
     : abstract_objectt(type, tp, bttm)
   {
-    PRECONDITION(type.id() == aggregate_traitst::TYPE_ID());
+    PRECONDITION(
+      type.id() != ID_struct_tag || ID_struct == aggregate_traitst::TYPE_ID());
+    PRECONDITION(
+      type.id() != ID_union_tag || ID_union == aggregate_traitst::TYPE_ID());
+    PRECONDITION(
+      type.id() == ID_struct_tag || type.id() == ID_union_tag ||
+      type.id() == aggregate_traitst::TYPE_ID());
   }
 
   abstract_aggregate_objectt(
@@ -42,7 +48,15 @@ class abstract_aggregate_objectt : public abstract_objectt,
     const namespacet &ns)
     : abstract_objectt(expr, environment, ns)
   {
-    PRECONDITION(ns.follow(expr.type()).id() == aggregate_traitst::TYPE_ID());
+    PRECONDITION(
+      expr.type().id() != ID_struct_tag ||
+      ID_struct == aggregate_traitst::TYPE_ID());
+    PRECONDITION(
+      expr.type().id() != ID_union_tag ||
+      ID_union == aggregate_traitst::TYPE_ID());
+    PRECONDITION(
+      expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag ||
+      expr.type().id() == aggregate_traitst::TYPE_ID());
   }
 
   abstract_object_pointert expression_transform(

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -209,19 +209,16 @@ bool abstract_environmentt::assign(
     final_value = value;
   }
 
-  const typet &lhs_type = ns.follow(lhs_value->type());
-  const typet &rhs_type = ns.follow(final_value->type());
-
   // Write the value for the root symbol back into the map
   INVARIANT(
-    lhs_type == rhs_type,
+    lhs_value->type() == final_value->type(),
     "Assignment types must match"
     "\n"
     "lhs_type :" +
-      lhs_type.pretty() +
+      lhs_value->type().pretty() +
       "\n"
       "rhs_type :" +
-      rhs_type.pretty());
+      final_value->type().pretty());
 
   // If LHS was directly the symbol
   if(s.id() == ID_symbol)

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -10,7 +10,6 @@
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
-#include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
@@ -225,8 +224,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
   if(stack.empty())
   {
     // We should not be changing the type of an abstract object
-    PRECONDITION(
-      new_value->type() == ns.follow(to_pointer_type(type()).base_type()));
+    PRECONDITION(new_value->type() == to_pointer_type(type()).base_type());
 
     // Get an expression that we can assign to
     exprt value = to_address_of_expr(value_stack.to_expression()).object();

src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

@@ -33,7 +33,7 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(
   bool bottom)
   : abstract_aggregate_baset(t, top, bottom)
 {
-  PRECONDITION(t.id() == ID_struct);
+  PRECONDITION(t.id() == ID_struct || t.id() == ID_struct_tag);
   DATA_INVARIANT(verify(), "Structural invariants maintained");
 }
 
@@ -43,9 +43,11 @@ full_struct_abstract_objectt::full_struct_abstract_objectt(
   const namespacet &ns)
   : abstract_aggregate_baset(e, environment, ns)
 {
-  PRECONDITION(ns.follow(e.type()).id() == ID_struct);
+  PRECONDITION(e.type().id() == ID_struct || e.type().id() == ID_struct_tag);
 
-  const struct_typet struct_type_def = to_struct_type(ns.follow(e.type()));
+  const struct_typet &struct_type_def =
+    e.type().id() == ID_struct ? to_struct_type(e.type())
+                               : ns.follow_tag(to_struct_tag_type(e.type()));
 
   bool did_initialize_values = false;
   auto struct_type_it = struct_type_def.components().begin();
@@ -204,7 +206,10 @@ void full_struct_abstract_objectt::output(
   // To ensure that a consistent ordering of fields is output, use
   // the underlying type declaration for this struct to determine
   // the ordering
-  struct_union_typet type_decl = to_struct_union_type(ns.follow(type()));
+  struct_union_typet type_decl =
+    (type().id() == ID_struct_tag || type().id() == ID_union_tag)
+      ? ns.follow_tag(to_struct_or_union_tag_type(type()))
+      : to_struct_union_type(type());
 
   bool first = true;
 

src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp

@@ -8,8 +8,6 @@
 
 #include "variable_sensitivity_object_factory.h"
 
-#include <util/namespace.h>
-
 #include "constant_abstract_value.h"
 #include "constant_pointer_abstract_object.h"
 #include "data_dependency_context.h"
@@ -44,7 +42,7 @@ abstract_object_pointert create_abstract_object(
   if(top || bottom)
     return std::make_shared<abstract_object_classt>(type, top, bottom);
 
-  PRECONDITION(type == ns.follow(e.type()));
+  PRECONDITION(type == e.type());
   return std::make_shared<abstract_object_classt>(e, environment, ns);
 }
 
@@ -124,11 +122,11 @@ variable_sensitivity_object_factoryt::get_abstract_object_type(
   {
     return configuration.pointer_abstract_type;
   }
-  else if(type.id() == ID_struct)
+  else if(type.id() == ID_struct || type.id() == ID_struct_tag)
   {
     return configuration.struct_abstract_type;
   }
-  else if(type.id() == ID_union)
+  else if(type.id() == ID_union || type.id() == ID_union_tag)
   {
     return configuration.union_abstract_type;
   }
@@ -149,52 +147,50 @@ variable_sensitivity_object_factoryt::get_abstract_object(
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  const typet &followed_type = ns.follow(type);
-  ABSTRACT_OBJECT_TYPET abstract_object_type =
-    get_abstract_object_type(followed_type);
+  ABSTRACT_OBJECT_TYPET abstract_object_type = get_abstract_object_type(type);
 
   switch(abstract_object_type)
   {
   case TWO_VALUE:
     return initialize_abstract_object<abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   case CONSTANT:
     return initialize_abstract_object<constant_abstract_valuet>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   case INTERVAL:
     return initialize_abstract_object<interval_abstract_valuet>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   case VALUE_SET:
     return initialize_abstract_object<value_set_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
 
   case ARRAY_INSENSITIVE:
     return initialize_abstract_object<two_value_array_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   case ARRAY_SENSITIVE:
     return initialize_abstract_object<full_array_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
 
   case POINTER_INSENSITIVE:
     return initialize_abstract_object<two_value_pointer_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   case POINTER_SENSITIVE:
     return initialize_abstract_object<constant_pointer_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   case VALUE_SET_OF_POINTERS:
     return initialize_abstract_object<value_set_pointer_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
 
   case STRUCT_INSENSITIVE:
     return initialize_abstract_object<two_value_struct_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   case STRUCT_SENSITIVE:
     return initialize_abstract_object<full_struct_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
 
   case UNION_INSENSITIVE:
     return initialize_abstract_object<two_value_union_abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
 
   case HEAP_ALLOCATION:
   {
@@ -210,7 +206,7 @@ variable_sensitivity_object_factoryt::get_abstract_object(
   default:
     UNREACHABLE;
     return initialize_abstract_object<abstract_objectt>(
-      followed_type, top, bottom, e, environment, ns, configuration);
+      type, top, bottom, e, environment, ns, configuration);
   }
 }