text: /*******************************************************************\
  
  Module: Unit tests for parsing generic classes
  
  Author: Diffblue Ltd.
  
  \*******************************************************************/
  
  #include <java-testing-utils/load_java_class.h>
  #include <java-testing-utils/require_type.h>
  #include <testing-utils/use_catch.h>
  
  SCENARIO(
    "parse_generic_fields",
    "[core][java_bytecode][java_bytecode_parse_generics]")
  {
    const symbol_tablet &new_symbol_table = load_java_class(
      "GenericFields", "./java_bytecode/java_bytecode_parse_generics");
  
    std::string class_prefix = "java::GenericFields";
  
    WHEN("Parsing the class with generic fields")
    {
      THEN("There is a generic class symbol GenericField")
      {
        REQUIRE(new_symbol_table.has_symbol(class_prefix));
  
        const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix);
        require_type::require_complete_java_generic_class(
          class_symbol.type, {class_prefix + "::T", class_prefix + "::S"});
  
        const struct_typet class_struct = to_struct_type(class_symbol.type);
  
        THEN("It has field f of type T")
        {
          const struct_union_typet::componentt &field =
            require_type::require_component(class_struct, "f");
          require_type::require_java_generic_parameter(
            field.type(), class_prefix + "::T");
        }
  
        THEN("It has field f2 pointing to Generic")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f2");
          require_type::require_pointer_to_tag(field.type(), "java::Generic");
          THEN("The pointer should be generic")
          {
            require_type::require_java_generic_type(
              field.type(),
              {{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
          }
        }
  
        THEN("It has field f3 pointing to Generic")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f3");
          require_type::require_pointer_to_tag(field.type(), "java::Generic");
          THEN("The pointer should be generic")
          {
            require_type::require_java_generic_type(
              field.type(),
              {{require_type::type_argument_kindt::Inst,
                "java::java.lang.Integer"}});
          }
        }
  
        THEN("It has field f4 pointing to Generic")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f4");
          require_type::require_pointer_to_tag(field.type(), "java::Generic");
          THEN("The pointer should be generic")
          {
            const java_generic_typet &generic_field =
              require_type::require_java_generic_type(
                field.type(),
                {{require_type::type_argument_kindt::Inst, "java::Generic"}});
  
            const typet &type_argument_1 =
              generic_field.generic_type_arguments().at(0);
            require_type::require_java_generic_type(
              type_argument_1,
              {{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
          }
        }
  
        THEN("It has field f5 pointing to Generic")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f5");
          require_type::require_pointer_to_tag(field.type(), "java::Generic");
          THEN("The pointer should be generic")
          {
            const java_generic_typet &generic_field =
              require_type::require_java_generic_type(
                field.type(),
                {{require_type::type_argument_kindt::Inst, "java::Generic"}});
  
            const typet &type_argument_1 =
              generic_field.generic_type_arguments().at(0);
            const java_generic_typet &generic_type_argument_1 =
              require_type::require_java_generic_type(
                type_argument_1,
                {{require_type::type_argument_kindt::Inst, "java::Generic"}});
  
            const typet &type_argument_1_1 =
              generic_type_argument_1.generic_type_arguments().at(0);
            require_type::require_java_generic_type(
              type_argument_1_1,
              {{require_type::type_argument_kindt::Inst,
                 "java::java.lang.Integer"}});
          }
        }
  
        THEN("It has field f6 pointing to GenericTwoParam")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f6");
          require_type::require_pointer_to_tag(
            field.type(), "java::GenericTwoParam");
          THEN("The pointer should be generic")
          {
            require_type::require_java_generic_type(
              field.type(),
              {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
               {require_type::type_argument_kindt::Var, class_prefix + "::T"}});
          }
        }
  
        THEN("It has field f7 pointing to GenericTwoParam")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f7");
          require_type::require_pointer_to_tag(
            field.type(), "java::GenericTwoParam");
          THEN("The pointer should be generic")
          {
            require_type::require_java_generic_type(
              field.type(),
              {{require_type::type_argument_kindt::Var, class_prefix + "::T"},
               {require_type::type_argument_kindt::Var, class_prefix + "::S"}});
          }
        }
  
        THEN("It has field f8 pointing to GenericTwoParam")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f8");
          require_type::require_pointer_to_tag(
            field.type(), "java::GenericTwoParam");
          THEN("The pointer should be generic")
          {
            require_type::require_java_generic_type(
              field.type(),
              {{require_type::type_argument_kindt::Inst,
                 "java::java.lang.Integer"},
               {require_type::type_argument_kindt::Var,
                 class_prefix + "::T"}});
          }
        }
  
        THEN("It has field f9 pointing to GenericTwoParam")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f9");
          require_type::require_pointer_to_tag(
            field.type(), "java::GenericTwoParam");
          THEN("The pointer should be generic")
          {
            require_type::require_java_generic_type(
              field.type(),
              {{require_type::type_argument_kindt::Var,
                 class_prefix + "::T"},
               {require_type::type_argument_kindt::Inst,
                "java::java.lang.Integer"}});
          }
        }
  
        THEN("It has field f10 pointing to GenericTwoParam")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f10");
          require_type::require_pointer_to_tag(
            field.type(), "java::GenericTwoParam");
          THEN("The pointer should be generic")
          {
            require_type::require_java_generic_type(
              field.type(),
              {{require_type::type_argument_kindt::Inst,
                "java::java.lang.Integer"},
               {require_type::type_argument_kindt::Inst,
                "java::java.lang.String"}});
          }
        }
  
        THEN("It has field f11 pointing to GenericTwoParam")
        {
          const struct_typet::componentt &field =
            require_type::require_component(class_struct, "f11");
          require_type::require_pointer_to_tag(
            field.type(), "java::GenericTwoParam");
          THEN("The pointer should be generic")
          {
            const java_generic_typet &generic_field =
              require_type::require_java_generic_type(
                field.type(),
                {{require_type::type_argument_kindt::Inst,
                   "java::Generic"},
                 {require_type::type_argument_kindt::Inst,
                   "java::GenericTwoParam"}});
  
            const typet &type_argument_1 =
              generic_field.generic_type_arguments().at(0);
            require_type::require_java_generic_type(
              type_argument_1,
              {{require_type::type_argument_kindt::Var,
                 class_prefix + "::T"}});
  
            const typet &type_argument_2 =
              generic_field.generic_type_arguments().at(1);
            require_type::require_java_generic_type(
              type_argument_2,
              {{require_type::type_argument_kindt::Var,
                 class_prefix + "::S"},
               {require_type::type_argument_kindt::Inst,
                 "java::java.lang.Integer"}});
          }
        }
      }
    }
  }
  