Java object factory: use follow_tag instead of follow

follow_tag(...) is stronger typed than follow(...), which means that some
explict upcasts can be dropped.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -415,7 +415,7 @@ void initialize_nondet_string_fields(
   namespacet ns(symbol_table);
 
   const struct_typet &struct_type =
-    to_struct_type(ns.follow(struct_expr.type()));
+    ns.follow_tag(to_struct_tag_type(struct_expr.type()));
 
   // In case the type for String was not added to the symbol table,
   // (typically when string refinement is not activated), `struct_type`
@@ -541,7 +541,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
-      replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
+      replacement_pointer_type,
+      ns.follow(to_struct_tag_type(replacement_pointer_type.subtype())));
 
     const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
       assignments, lifetime, replacement_pointer_type, depth, location);
@@ -570,7 +571,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
   // the pointer to NULL instead of recursively initializing the struct to which
   // it points.
-  const typet &subtype=ns.follow(pointer_type.subtype());
+  const typet &subtype = ns.follow(to_struct_tag_type(pointer_type.subtype()));
   if(subtype.id()==ID_struct)
   {
     const struct_typet &struct_type=to_struct_type(subtype);
@@ -831,7 +832,7 @@ void java_object_factoryt::gen_nondet_struct_init(
   const update_in_placet &update_in_place,
   const source_locationt &location)
 {
-  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
+  PRECONDITION(expr.type().id() == ID_struct_tag);
   PRECONDITION(struct_type.id()==ID_struct);
 
   typedef struct_typet::componentst componentst;
@@ -1044,7 +1045,7 @@ void java_object_factoryt::gen_nondet_init(
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
-      pointer_type, ns.follow(pointer_type.subtype()));
+      pointer_type, ns.follow_tag(to_struct_tag_type(pointer_type.subtype())));
 
     gen_nondet_pointer_init(
       assignments,
@@ -1055,23 +1056,23 @@ void java_object_factoryt::gen_nondet_init(
       update_in_place,
       location);
   }
-  else if(type.id()==ID_struct)
+  else if(type.id() == ID_struct_tag)
   {
-    const struct_typet struct_type=to_struct_type(type);
+    const struct_tag_typet &struct_tag_type = to_struct_tag_type(type);
+
+    const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
 
     // If we are about to initialize a generic class (as a superclass object
     // for a different object), add its concrete types to the map and delete
     // them on leaving this function scope.
     generic_parameter_specialization_map_keyst
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
+
     if(is_sub)
     {
-      const typet &symbol =
-        override_type.has_value() ? *override_type : expr.type();
-      PRECONDITION(symbol.id() == ID_struct_tag);
       generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
-        to_struct_tag_type(symbol), struct_type);
+        struct_tag_type, struct_type);
     }
 
     gen_nondet_struct_init(
@@ -1392,8 +1393,9 @@ void java_object_factoryt::gen_nondet_array_init(
   PRECONDITION(expr.type().subtype().id() == ID_struct_tag);
   PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
 
-  const typet &type = ns.follow(expr.type().subtype());
-  const struct_typet &struct_type = to_struct_type(type);
+  const struct_tag_typet &struct_tag_type =
+    to_struct_tag_type(expr.type().subtype());
+  const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
   const typet &element_type =
     static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
 
@@ -1476,7 +1478,8 @@ void java_object_factoryt::gen_nondet_enum_init(
 
   // Access members (length and data) of $VALUES array
   dereference_exprt deref_expr(values.symbol_expr());
-  const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type()));
+  const auto &deref_struct_type =
+    ns.follow_tag(to_struct_tag_type(deref_expr.type()));
   PRECONDITION(is_valid_java_array(deref_struct_type));
   const auto &comps = deref_struct_type.components();
   const member_exprt length_expr(deref_expr, "length", comps[1].type());