diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 32164a382cf..1cc35143fa9 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -14,20 +14,6 @@ #include #include -/// Strip the package name from a java type, for the type to be -/// pretty printed (java::java.lang.Integer -> Integer). -/// \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) -{ - const std::string java_lang("java::java.lang."); - const std::string package_name(java_class_to_package(fqn_java_type) + "."); - if(package_name == java_lang) - return fqn_java_type.substr(java_lang.length()); - return fqn_java_type; -} - generate_java_generic_typet::generate_java_generic_typet( message_handlert &message_handler): message_handler(message_handler) diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index f720d32ada8..0021bff9325 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -305,3 +305,23 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip) PRECONDITION(has_prefix(to_strip_str, prefix)); return to_strip_str.substr(prefix.size(), std::string::npos); } + +/// Strip the package name from a java type, for the type to be +/// pretty printed (java::java.lang.Integer -> Integer). +/// \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. +std::string pretty_print_java_type(const std::string &fqn_java_type) +{ + std::string result(fqn_java_type); + const std::string java_cbmc_string("java::"); + // Remove the CBMC internal java identifier + if(has_prefix(fqn_java_type, java_cbmc_string)) + result = fqn_java_type.substr(java_cbmc_string.length()); + // If the class is in package java.lang strip + // package name due to default import + const std::string java_lang_string("java.lang."); + if(has_prefix(result, java_lang_string)) + result = result.substr(java_lang_string.length()); + return result; +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index 6f163df484f..ad4c45f51c0 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -94,4 +94,6 @@ exprt make_function_application( irep_idt strip_java_namespace_prefix(const irep_idt &to_strip); +std::string pretty_print_java_type(const std::string &fqn_java_type); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index de216862376..f4b8625ceec 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -7,6 +7,9 @@ \*******************************************************************/ +#include +#include + #include #include #include @@ -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"; 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"; const irep_idt test_class_int = - "java::generic_field_array_instantiation$generic"; + "java::generic_field_array_instantiation$generic"; const irep_idt test_class_float = - "java::generic_field_array_instantiation$generic"; + "java::generic_field_array_instantiation$generic"; const struct_typet::componentt &component_g = require_type::require_component( @@ -330,7 +333,7 @@ SCENARIO( "table") { const std::string specialised_string = - ""; const irep_idt specialised_class_name = id2string(harness_class) + "$" + id2string(inner_class) + diff --git a/unit/java_bytecode/java_utils_test.cpp b/unit/java_bytecode/java_utils_test.cpp index b568b8c6d01..3f3c7e603a6 100644 --- a/unit/java_bytecode/java_utils_test.cpp +++ b/unit/java_bytecode/java_utils_test.cpp @@ -341,3 +341,30 @@ SCENARIO("find_closing_semi_colon_for_reference_type", "[core][java_util_test]") REQUIRE(find_closing_semi_colon_for_reference_type(descriptor, 10) == 19); } } + +SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]") +{ + using std::map; + using std::string; + + WHEN("We have a series of cbmc internal java types") + { + // NOLINTNEXTLINE + const map types{ + // map + {"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); + } + } + } +}