Fixed the pretty printing type function and fix the tests failing, and introduce test for the pretty printing function.

Author: NlightNFotis

src/java_bytecode/generate_java_generic_type.cpp

@@ -11,6 +11,7 @@
 
 #include "generate_java_generic_type.h"
 #include <util/namespace.h>
+#include <util/prefix.h>
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>
 
@@ -19,17 +20,17 @@
 /// \param fqn_java_type The java type we want to pretty print.
 /// \return The pretty printed type if there was a match of the
 //  qualifiers, or the type as it was passed otherwise.
-static std::string pretty_print_java_type(const std::string &fqn_java_type)
+std::string pretty_print_java_type(const std::string &fqn_java_type)
 {
-  std::string result;
+  std::string result(fqn_java_type);
   const std::string java_cbmc_string("java::");
   // Remove the java internal cbmc identifier
-  if(fqn_java_type.substr(0, java_cbmc_string.length()) == java_cbmc_string)
+  if(has_prefix(fqn_java_type, java_cbmc_string))
     result = fqn_java_type.substr(java_cbmc_string.length());
-  // If the remaining has the "java.lang." string as well, trim it
+  // If the class is in package java.lang strip
+  // package name due to default import
   const std::string java_lang_string("java.lang.");
-  const std::string package_name(java_class_to_package(result) + ".");
-  if(package_name == java_lang_string)
+  if(has_prefix(result, java_lang_string))
     result = result.substr(java_lang_string.length());
   return result;
 }

src/java_bytecode/generate_java_generic_type.h

@@ -43,4 +43,6 @@ class generate_java_generic_typet
   message_handlert &message_handler;
 };
 
+std::string pretty_print_java_type(const std::string &fqn_java_type);
+
 #endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -7,6 +7,9 @@
 
 \*******************************************************************/
 
+#include <map>
+#include <string>
+
 #include <testing-utils/catch.hpp>
 #include <testing-utils/load_java_class.h>
 #include <testing-utils/require_type.h>
@@ -179,7 +182,7 @@ SCENARIO(
   // We want to test that the specialized/instantiated class has it's field
   // type updated, so find the specialized class, not the generic class.
   const irep_idt test_class =
-    "java::generic_field_array_instantiation$generic<java::array[reference]"
+    "java::generic_field_array_instantiation$generic<array[reference]"
     "of_java::java.lang.Float>";
 
   GIVEN("A generic type instantiated with an array type")
@@ -224,15 +227,15 @@ SCENARIO(
     GIVEN("A generic type instantiated with different array types")
     {
       const irep_idt test_class_integer =
-        "java::generic_field_array_instantiation$generic<java::array[reference]"
+        "java::generic_field_array_instantiation$generic<array[reference]"
         "of_"
         "java::java.lang.Integer>";
 
       const irep_idt test_class_int =
-        "java::generic_field_array_instantiation$generic<java::array[int]>";
+        "java::generic_field_array_instantiation$generic<array[int]>";
 
       const irep_idt test_class_float =
-        "java::generic_field_array_instantiation$generic<java::array[float]>";
+        "java::generic_field_array_instantiation$generic<array[float]>";
 
       const struct_typet::componentt &component_g =
         require_type::require_component(
@@ -330,7 +333,7 @@ SCENARIO(
         "table")
       {
         const std::string specialised_string =
-          "<java::array[reference]of_"
+          "<array[reference]of_"
           "java::java.lang.Float>";
         const irep_idt specialised_class_name = id2string(harness_class) + "$" +
                                                 id2string(inner_class) +
@@ -389,3 +392,32 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "Test pretty printing auxiliary function",
+  "[core][java_bytecode][generate_java_generic_type]")
+{
+  using std::map;
+  using std::string;
+
+  WHEN("We have a series of cbmc internal java types")
+  {
+    // NOLINTNEXTLINE
+    const map<string, string> types{
+      // map<Input, Output>
+      {"java::java.lang.Integer", "Integer"},
+      {"java::CustomClass", "CustomClass"},
+      {"java.lang.String", "String"},
+      {"Hashmap", "Hashmap"},
+      // We shouldn't prune types not imported in default import
+      {"java.util.HashSet", "java.util.HashSet"}};
+
+    THEN("We need to make sure that the types get pruned correctly.")
+    {
+      for(const auto &pair : types)
+      {
+        REQUIRE(pretty_print_java_type(pair.first) == pair.second);
+      }
+    }
+  }
+}