Skip to content

Commit 7d37272

Browse files
committed
Fix the pretty printing routine to pp types that have java:: as their prefix only
1 parent a1bc2a2 commit 7d37272

File tree

1 file changed

+11
-5
lines changed

1 file changed

+11
-5
lines changed

src/java_bytecode/generate_java_generic_type.cpp

+11-5
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,17 @@
2121
// qualifiers, or the type as it was passed otherwise.
2222
static std::string pretty_print_java_type(const std::string &fqn_java_type)
2323
{
24-
const std::string java_lang("java::java.lang.");
25-
const std::string package_name(java_class_to_package(fqn_java_type) + ".");
26-
if(package_name == java_lang)
27-
return fqn_java_type.substr(java_lang.length());
28-
return fqn_java_type;
24+
std::string result;
25+
const std::string java_cbmc_string("java::");
26+
// Remove the java internal cbmc identifier
27+
if(fqn_java_type.substr(0, java_cbmc_string.length()) == java_cbmc_string)
28+
result = fqn_java_type.substr(java_cbmc_string.length());
29+
// If the remaining has the "java.lang." string as well, trim it
30+
const std::string java_lang_string("java.lang.");
31+
const std::string package_name(java_class_to_package(result) + ".");
32+
if(package_name == java_lang_string)
33+
result = result.substr(java_lang_string.length());
34+
return result;
2935
}
3036

3137
generate_java_generic_typet::generate_java_generic_typet(

0 commit comments

Comments
 (0)