From 363d217ef6e771019da50da8ed557c7f213139ed Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Tue, 12 Feb 2019 17:50:19 +0000
Subject: [PATCH] Generic tests: check for matching tag, not completely
 matching type

Previously these relied on base_type_eq to hide differently-decorated tags; now they explicitly
just check the tag name, rather than relying on base_type_eq, which will soon go away anyway, to
hide generic qualifiers and/or array element types.
---
 jbmc/unit/java-testing-utils/require_type.cpp |   8 +
 jbmc/unit/java-testing-utils/require_type.h   |   4 +
 .../parse_bounded_generic_inner_classes.cpp   |   4 +-
 .../parse_functions_with_generics.cpp         |  37 ++--
 .../parse_generic_array_class.cpp             |  21 +--
 .../parse_generic_class.cpp                   |   3 +-
 ...neric_class_with_generic_inner_classes.cpp | 162 ++++++++----------
 ...parse_generic_class_with_inner_classes.cpp |  23 ++-
 .../parse_generic_fields.cpp                  |  36 ++--
 .../parse_nested_generics.cpp                 | 149 ++++++++--------
 10 files changed, 203 insertions(+), 244 deletions(-)

diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp
index 52b02439eff..09e1381a009 100644
--- a/jbmc/unit/java-testing-utils/require_type.cpp
+++ b/jbmc/unit/java-testing-utils/require_type.cpp
@@ -461,6 +461,14 @@ require_type::require_struct_tag(const typet &type, const irep_idt &identifier)
   return result;
 }
 
+const pointer_typet
+require_type::require_pointer_to_tag(const typet &type, const irep_idt &tag)
+{
+  const auto pointer_type = require_type::require_pointer(type, {});
+  require_type::require_struct_tag(pointer_type.subtype(), tag);
+  return pointer_type;
+}
+
 /// Verify a given type is a java generic symbol type
 /// \param type: The type to check
 /// \param identifier: The identifier to match
diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h
index 624215714fd..14ae5c47f7b 100644
--- a/jbmc/unit/java-testing-utils/require_type.h
+++ b/jbmc/unit/java-testing-utils/require_type.h
@@ -28,6 +28,10 @@ require_pointer(const typet &type, const optionalt<typet> &subtype);
 const struct_tag_typet &
 require_struct_tag(const typet &type, const irep_idt &identifier = "");
 
+const pointer_typet require_pointer_to_tag(
+  const typet &type,
+  const irep_idt &identifier = irep_idt());
+
 struct_typet::componentt require_component(
   const struct_typet &struct_type,
   const irep_idt &component_name);
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
index 04d6973e69c..ee15c4241dd 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp
@@ -91,8 +91,8 @@ SCENARIO(
     const struct_union_typet::componentt &belem_type =
       require_type::require_component(
         to_struct_type(class_symbol.type), "belem");
-    require_type::require_pointer(
-      belem_type.type(), struct_tag_typet(class_prefix + "$BoundedInner"));
+    require_type::require_pointer_to_tag(
+      belem_type.type(), class_prefix + "$BoundedInner");
     require_type::require_java_generic_type(
       belem_type.type(),
       {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
index 425a8abe974..90cb25c545b 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp
@@ -39,8 +39,7 @@ SCENARIO(
       {
         const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
-        require_type::require_pointer(
-          param_x.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(param_x.type(), "java::Generic");
 
         THEN("x is generic with parameter pointing to java.lang.Integer")
         {
@@ -54,8 +53,7 @@ SCENARIO(
       THEN("It has return type pointing to Generic")
       {
         const typet return_type = func_code.return_type();
-        require_type::require_pointer(
-          return_type, struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(return_type, "java::Generic");
 
         THEN("It is generic with parameter pointing to java.lang.Integer")
         {
@@ -88,8 +86,7 @@ SCENARIO(
       {
         const java_method_typet::parametert &param_s =
           require_type::require_parameter(func_code, "s");
-        require_type::require_pointer(
-          param_s.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(param_s.type(), "java::Generic");
 
         THEN("s is generic with parameter pointing to java.lang.String")
         {
@@ -103,8 +100,7 @@ SCENARIO(
       THEN("It has return type pointing to Generic")
       {
         const typet return_type = func_code.return_type();
-        require_type::require_pointer(
-          return_type, struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(return_type, "java::Generic");
 
         THEN("It is generic with parameter pointing to java.lang.Integer")
         {
@@ -137,8 +133,7 @@ SCENARIO(
       {
         const java_method_typet::parametert &param_x =
           require_type::require_parameter(func_code, "x");
-        require_type::require_pointer(
-          param_x.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(param_x.type(), "java::Generic");
 
         THEN("x is generic with parameter pointing to java.lang.Integer")
         {
@@ -153,8 +148,7 @@ SCENARIO(
       {
         const java_method_typet::parametert &param_y =
           require_type::require_parameter(func_code, "y");
-        require_type::require_pointer(
-          param_y.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(param_y.type(), "java::Generic");
 
         THEN("y is generic with parameter pointing to java.lang.Integer")
         {
@@ -168,8 +162,7 @@ SCENARIO(
       THEN("It has return type pointing to Generic")
       {
         const typet return_type = func_code.return_type();
-        require_type::require_pointer(
-          return_type, struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(return_type, "java::Generic");
 
         THEN("It is generic with parameter pointing to java.lang.Integer")
         {
@@ -202,8 +195,7 @@ SCENARIO(
       {
         const java_method_typet::parametert &param_s =
           require_type::require_parameter(func_code, "s");
-        require_type::require_pointer(
-          param_s.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(param_s.type(), "java::Generic");
 
         THEN("s is generic with parameter pointing to java.lang.String")
         {
@@ -218,8 +210,7 @@ SCENARIO(
       {
         const java_method_typet::parametert &param_b =
           require_type::require_parameter(func_code, "b");
-        require_type::require_pointer(
-          param_b.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(param_b.type(), "java::Generic");
 
         THEN("b is generic with parameter pointing to java.lang.Boolean")
         {
@@ -233,8 +224,7 @@ SCENARIO(
       THEN("It has return type pointing to Generic")
       {
         const typet return_type = func_code.return_type();
-        require_type::require_pointer(
-          return_type, struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(return_type, "java::Generic");
 
         THEN("It is generic with parameter pointing to java.lang.Integer")
         {
@@ -268,15 +258,14 @@ SCENARIO(
       {
         const java_method_typet::parametert &param_inner =
           require_type::require_parameter(func_code, "inner");
-        require_type::require_pointer(
-          param_inner.type(), struct_tag_typet(class_prefix + "$Inner"));
+        require_type::require_pointer_to_tag(
+          param_inner.type(), class_prefix + "$Inner");
       }
 
       THEN("It has return type pointing to Generic")
       {
         const typet return_type = func_code.return_type();
-        require_type::require_pointer(
-          return_type, struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(return_type, "java::Generic");
 
         THEN("It is generic with parameter pointing to java.lang.Integer")
         {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
index 1e733b6dc79..9d1655eb1b4 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
@@ -32,8 +32,9 @@ SCENARIO(
 
     THEN("It is an array")
     {
-      const pointer_typet &field_t_pointer = require_type::require_pointer(
-        field_t.type(), struct_tag_typet("java::array[reference]"));
+      const pointer_typet &field_t_pointer =
+        require_type::require_pointer_to_tag(
+          field_t.type(), "java::array[reference]");
 
       const struct_tag_typet &field_t_subtype =
         to_struct_tag_type(field_t_pointer.subtype());
@@ -57,8 +58,9 @@ SCENARIO(
 
     THEN("It is an array")
     {
-      const pointer_typet &field_t2_pointer = require_type::require_pointer(
-        field_t2.type(), struct_tag_typet("java::array[reference]"));
+      const pointer_typet &field_t2_pointer =
+        require_type::require_pointer_to_tag(
+          field_t2.type(), "java::array[reference]");
 
       const struct_tag_typet &field_t2_subtype =
         to_struct_tag_type(field_t2_pointer.subtype());
@@ -69,8 +71,7 @@ SCENARIO(
       THEN("The elements have type Generic<T>")
       {
         const typet &element = java_array_element_type(field_t2_subtype);
-        require_type::require_pointer(
-          element, struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(element, "java::Generic");
         require_type::require_java_generic_type(
           element,
           {{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
@@ -85,8 +86,9 @@ SCENARIO(
 
     THEN("It is an array")
     {
-      const pointer_typet &field_t3_pointer = require_type::require_pointer(
-        field_t3.type(), struct_tag_typet("java::array[reference]"));
+      const pointer_typet &field_t3_pointer =
+        require_type::require_pointer_to_tag(
+          field_t3.type(), "java::array[reference]");
 
       const struct_tag_typet &field_t3_subtype =
         to_struct_tag_type(field_t3_pointer.subtype());
@@ -97,8 +99,7 @@ SCENARIO(
       THEN("The elements have type Generic<Integer>")
       {
         const typet &element = java_array_element_type(field_t3_subtype);
-        require_type::require_pointer(
-          element, struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(element, "java::Generic");
         require_type::require_java_generic_type(
           element,
           {{require_type::type_argument_kindt::Inst,
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp
index 374e2b34031..fde0089906a 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp
@@ -46,8 +46,7 @@ SCENARIO(
       {
         const struct_union_typet::componentt &field_g =
           require_type::require_component(class_struct, "g");
-        require_type::require_pointer(
-          field_g.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(field_g.type(), "java::Generic");
 
         THEN("It is generic with parameter pointing to java.lang.Integer")
         {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
index 22cd28c16c8..730637d72a4 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp
@@ -36,8 +36,8 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field");
 
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet(class_prefix + "$InnerClass"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), class_prefix + "$InnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -54,9 +54,8 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field2");
 
-      require_type::require_pointer(
-        field_component.type(),
-        struct_tag_typet(class_prefix + "$GenericInnerClass"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), class_prefix + "$GenericInnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -76,9 +75,8 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field3");
 
-      require_type::require_pointer(
-        field_component.type(),
-        struct_tag_typet(class_prefix + "$GenericInnerClass"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), class_prefix + "$GenericInnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -96,10 +94,9 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field4");
 
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         field_component.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -119,10 +116,9 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field5");
 
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         field_component.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -140,10 +136,9 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field6");
 
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         field_component.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass");
 
       THEN("The pointer should be generic")
       {
@@ -165,10 +160,9 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field7");
 
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         field_component.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass");
 
       THEN("The pointer should be generic")
       {
@@ -187,9 +181,8 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field8");
 
-      require_type::require_pointer(
-        field_component.type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), class_prefix + "$TwoParamInnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -211,9 +204,8 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field9");
 
-      require_type::require_pointer(
-        field_component.type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), class_prefix + "$TwoParamInnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -235,9 +227,8 @@ SCENARIO(
       const struct_typet::componentt &field_component =
         require_type::require_component(java_generic_class, "field10");
 
-      require_type::require_pointer(
-        field_component.type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), class_prefix + "$TwoParamInnerClass");
 
       THEN("The pointer should be generic")
       {
@@ -261,10 +252,9 @@ SCENARIO(
       //   GenericInnerClass<GenericClassWithGenericInnerClasses<Integer>>.
       //     DoublyNestedInnerGenericClass<T> field11;
 
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         field_component.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass");
 
       THEN("The pointer should be GenericClassWithGenericInnerClasses")
       {
@@ -323,8 +313,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet(class_prefix + "$InnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), class_prefix + "$InnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
@@ -352,16 +342,16 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet(class_prefix + "$InnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), class_prefix + "$InnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
 
       const auto &param_type2 =
         require_type::require_parameter(function_call, "input2");
-      require_type::require_pointer(
-        param_type2.type(), struct_tag_typet(class_prefix + "$InnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type2.type(), class_prefix + "$InnerClass");
       require_type::require_java_generic_type(
         param_type2.type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
@@ -388,9 +378,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(),
-        struct_tag_typet(class_prefix + "$GenericInnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), class_prefix + "$GenericInnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var,
@@ -420,9 +409,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(),
-        struct_tag_typet(class_prefix + "$GenericInnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), class_prefix + "$GenericInnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
@@ -451,10 +439,9 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         param_type.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var,
@@ -485,10 +472,9 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         param_type.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
@@ -517,10 +503,9 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         param_type.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var,
@@ -553,10 +538,9 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         param_type.type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
@@ -585,9 +569,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), class_prefix + "$TwoParamInnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var,
@@ -619,9 +602,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), class_prefix + "$TwoParamInnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var,
@@ -653,9 +635,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), class_prefix + "$TwoParamInnerClass");
       require_type::require_java_generic_type(
         param_type.type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
@@ -682,9 +663,8 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(),
-        struct_tag_typet(class_prefix + "$InnerClass"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), class_prefix + "$InnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
@@ -709,9 +689,8 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(),
-        struct_tag_typet(class_prefix + "$GenericInnerClass"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), class_prefix + "$GenericInnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var,
@@ -739,9 +718,8 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(),
-        struct_tag_typet(class_prefix + "$GenericInnerClass"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), class_prefix + "$GenericInnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
@@ -768,10 +746,10 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         function_call.return_type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerClass"));
+
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var,
@@ -800,10 +778,9 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         function_call.return_type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
@@ -830,10 +807,9 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         function_call.return_type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var,
@@ -864,10 +840,9 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
+      require_type::require_pointer_to_tag(
         function_call.return_type(),
-        struct_tag_typet(
-          class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass"));
+        class_prefix + "$GenericInnerClass$DoublyNestedInnerGenericClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
@@ -895,9 +870,8 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), class_prefix + "$TwoParamInnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var,
@@ -927,9 +901,8 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), class_prefix + "$TwoParamInnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var,
@@ -959,9 +932,8 @@ SCENARIO(
 
     THEN("The return type should be correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(),
-        struct_tag_typet(class_prefix + "$TwoParamInnerClass"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), class_prefix + "$TwoParamInnerClass");
       require_type::require_java_generic_type(
         function_call.return_type(),
         {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
index 13a34cdcaa2..313ed682723 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
@@ -31,8 +31,8 @@ SCENARIO(
     THEN("There is a field f1 of generic type with correct arguments")
     {
       const auto &field = require_type::require_component(generic_class, "f1");
-      require_type::require_pointer(
-        field.type(), struct_tag_typet(outer_class_prefix + "$Inner"));
+      require_type::require_pointer_to_tag(
+        field.type(), outer_class_prefix + "$Inner");
       require_type::require_java_generic_type(
         field.type(),
         {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}});
@@ -40,9 +40,8 @@ SCENARIO(
     THEN("There is a field f2 of generic type with correct arguments")
     {
       const auto &field = require_type::require_component(generic_class, "f2");
-      require_type::require_pointer(
-        field.type(),
-        struct_tag_typet(outer_class_prefix + "$Inner$InnerInner"));
+      require_type::require_pointer_to_tag(
+        field.type(), outer_class_prefix + "$Inner$InnerInner");
       require_type::require_java_generic_type(
         field.type(),
         {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}});
@@ -50,8 +49,8 @@ SCENARIO(
     THEN("There is a field f3 of generic type with correct arguments")
     {
       const auto &field = require_type::require_component(generic_class, "f3");
-      require_type::require_pointer(
-        field.type(), struct_tag_typet(outer_class_prefix + "$GenericInner"));
+      require_type::require_pointer_to_tag(
+        field.type(), outer_class_prefix + "$GenericInner");
       require_type::require_java_generic_type(
         field.type(),
         {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"},
@@ -85,8 +84,7 @@ SCENARIO(
         "parameter of the outer class")
       {
         const auto &field = require_type::require_component(java_class, "t2");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(field.type(), "java::Generic");
         require_type::require_java_generic_type(
           field.type(),
           {{require_type::type_argument_kindt::Var,
@@ -122,8 +120,7 @@ SCENARIO(
         "parameter of the outer class")
       {
         const auto &field = require_type::require_component(java_class, "tt2");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(field.type(), "java::Generic");
         const java_generic_typet &generic_field =
           require_type::require_java_generic_type(
             field.type(),
@@ -171,8 +168,8 @@ SCENARIO(
       {
         const auto &field =
           require_type::require_component(generic_class, "gt2");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::GenericTwoParam"));
+        require_type::require_pointer_to_tag(
+          field.type(), "java::GenericTwoParam");
         require_type::require_java_generic_type(
           field.type(),
           {{require_type::type_argument_kindt::Var,
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp
index c4416f4817f..be0c8372c38 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp
@@ -43,8 +43,7 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f2");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(field.type(), "java::Generic");
         THEN("The pointer should be generic")
         {
           require_type::require_java_generic_type(
@@ -57,8 +56,7 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f3");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(field.type(), "java::Generic");
         THEN("The pointer should be generic")
         {
           require_type::require_java_generic_type(
@@ -72,8 +70,7 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f4");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(field.type(), "java::Generic");
         THEN("The pointer should be generic")
         {
           const java_generic_typet &generic_field =
@@ -93,8 +90,7 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f5");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::Generic"));
+        require_type::require_pointer_to_tag(field.type(), "java::Generic");
         THEN("The pointer should be generic")
         {
           const java_generic_typet &generic_field =
@@ -122,8 +118,8 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f6");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::GenericTwoParam"));
+        require_type::require_pointer_to_tag(
+          field.type(), "java::GenericTwoParam");
         THEN("The pointer should be generic")
         {
           require_type::require_java_generic_type(
@@ -137,8 +133,8 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f7");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::GenericTwoParam"));
+        require_type::require_pointer_to_tag(
+          field.type(), "java::GenericTwoParam");
         THEN("The pointer should be generic")
         {
           require_type::require_java_generic_type(
@@ -152,8 +148,8 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f8");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::GenericTwoParam"));
+        require_type::require_pointer_to_tag(
+          field.type(), "java::GenericTwoParam");
         THEN("The pointer should be generic")
         {
           require_type::require_java_generic_type(
@@ -169,8 +165,8 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f9");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::GenericTwoParam"));
+        require_type::require_pointer_to_tag(
+          field.type(), "java::GenericTwoParam");
         THEN("The pointer should be generic")
         {
           require_type::require_java_generic_type(
@@ -186,8 +182,8 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f10");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::GenericTwoParam"));
+        require_type::require_pointer_to_tag(
+          field.type(), "java::GenericTwoParam");
         THEN("The pointer should be generic")
         {
           require_type::require_java_generic_type(
@@ -203,8 +199,8 @@ SCENARIO(
       {
         const struct_typet::componentt &field =
           require_type::require_component(class_struct, "f11");
-        require_type::require_pointer(
-          field.type(), struct_tag_typet("java::GenericTwoParam"));
+        require_type::require_pointer_to_tag(
+          field.type(), "java::GenericTwoParam");
         THEN("The pointer should be generic")
         {
           const java_generic_typet &generic_field =
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
index 05032fab72c..5047704abdf 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp
@@ -30,8 +30,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -53,8 +53,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field2");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -76,8 +76,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field3");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -106,8 +106,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field4");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -136,8 +136,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field5");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -162,8 +162,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field6");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -188,8 +188,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field7");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -214,8 +214,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field8");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -245,8 +245,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field9");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -276,8 +276,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field10");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -307,8 +307,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field11");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -333,8 +333,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field12");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -366,8 +366,8 @@ SCENARIO(
     {
       const struct_typet::componentt &field_component =
         require_type::require_component(class_type, "field13");
-      require_type::require_pointer(
-        field_component.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        field_component.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -424,8 +424,7 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(param_type.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -462,8 +461,7 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(param_type.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -500,8 +498,7 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(param_type.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -545,8 +542,7 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(param_type.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -590,8 +586,7 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(param_type.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -631,8 +626,7 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(param_type.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -672,8 +666,7 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(param_type.type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -713,8 +706,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -758,8 +751,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -803,8 +796,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -848,8 +841,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -889,8 +882,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -936,8 +929,8 @@ SCENARIO(
     {
       const auto &param_type =
         require_type::require_parameter(function_call, "input");
-      require_type::require_pointer(
-        param_type.type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        param_type.type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -981,8 +974,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -1017,8 +1010,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -1053,8 +1046,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -1095,8 +1088,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -1137,8 +1130,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -1176,8 +1169,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -1215,8 +1208,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::Generic"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::Generic");
 
       THEN("The pointer should be generic")
       {
@@ -1254,8 +1247,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -1297,8 +1290,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -1340,8 +1333,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -1383,8 +1376,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -1422,8 +1415,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {
@@ -1467,8 +1460,8 @@ SCENARIO(
 
     THEN("The return type is correct")
     {
-      require_type::require_pointer(
-        function_call.return_type(), struct_tag_typet("java::GenericTwoParam"));
+      require_type::require_pointer_to_tag(
+        function_call.return_type(), "java::GenericTwoParam");
 
       THEN("The pointer should be generic")
       {