Updating utility functions to check generic/non-generic java classes

Author: svorenova

unit/testing-utils/require_type.cpp

@@ -202,14 +202,65 @@ const typet &require_type::require_java_non_generic_type(
   return type;
 }
 
-/// Verify that a class is a valid java generic class
+/// Checks that the given type is a complete class.
+/// \param class_type type of the class
+/// \return class_type of the class
+class_typet require_complete_class(const typet &class_type)
+{
+  REQUIRE(class_type.id() == ID_struct);
+
+  const class_typet &class_class_type = to_class_type(class_type);
+  REQUIRE(class_class_type.is_class());
+  REQUIRE_FALSE(class_class_type.get_bool(ID_incomplete_class));
+
+  return class_class_type;
+}
+
+/// Verify that a class is a complete, valid java generic class with the
+/// specified list of variables.
 /// \param class_type: the class
+/// \param type_variables: vector of type variables
 /// \return: A reference to the java generic class type.
-java_generics_class_typet &
-require_type::require_java_generic_class(const class_typet &class_type)
+java_generics_class_typet require_type::require_java_generic_class(
+  const typet &class_type,
+  const optionalt<std::initializer_list<irep_idt>> &type_variables)
 {
-  java_class_typet java_class_type = to_java_class_type(class_type);
+  const class_typet &class_class_type = require_complete_class(class_type);
+  java_class_typet java_class_type = to_java_class_type(class_class_type);
 
   REQUIRE(is_java_generics_class_type(java_class_type));
-  return to_java_generics_class_type(java_class_type);
+  java_generics_class_typet java_generic_class_type =
+    to_java_generics_class_type(java_class_type);
+
+  if(type_variables)
+  {
+    const java_generics_class_typet::generic_typest &generic_type_vars =
+      java_generic_class_type.generic_types();
+    REQUIRE(generic_type_vars.size() == type_variables.value().size());
+    REQUIRE(
+      std::equal(
+        type_variables->begin(),
+        type_variables->end(),
+        generic_type_vars.begin(),
+        [](
+          const irep_idt &type_var_name, const java_generic_parametert &param) {
+          REQUIRE(!is_java_generic_inst_parameter((param)));
+          return param.type_variable().get_identifier() == type_var_name;
+        }));
+  }
+  return java_generic_class_type;
+}
+
+/// Verify that a class is a complete, valid nongeneric java class
+/// \param class_type: the class
+/// \return: A reference to the java generic class type.
+java_class_typet
+require_type::require_java_non_generic_class(const typet &class_type)
+{
+  const class_typet &class_class_type = require_complete_class(class_type);
+  java_class_typet java_class_type = to_java_class_type(class_class_type);
+
+  REQUIRE(!is_java_generics_class_type(java_class_type));
+
+  return java_class_type;
 }

unit/testing-utils/require_type.h

@@ -19,7 +19,6 @@
 #include <util/std_types.h>
 #include <java_bytecode/java_types.h>
 
-
 // NOLINTNEXTLINE(readability/namespace)
 namespace require_type
 {
@@ -63,8 +62,11 @@ const typet &require_java_non_generic_type(
   const typet &type,
   const optionalt<symbol_typet> &expect_subtype);
 
-java_generics_class_typet &
-require_java_generic_class(const class_typet &class_type);
+java_generics_class_typet require_java_generic_class(
+  const typet &class_type,
+  const optionalt<std::initializer_list<irep_idt>> &type_variables);
+
+java_class_typet require_java_non_generic_class(const typet &class_type);
 }
 
 #endif // CPROVER_TESTING_UTILS_REQUIRE_TYPE_H