Skip to content

Commit 8a9aa0f

Browse files
committed
Move the pretty printing function from generate_java_generic_type to java_utils.
1 parent 0a0fa08 commit 8a9aa0f

File tree

6 files changed

+49
-52
lines changed

6 files changed

+49
-52
lines changed

src/java_bytecode/generate_java_generic_type.cpp

-21
Original file line numberDiff line numberDiff line change
@@ -11,30 +11,9 @@
1111

1212
#include "generate_java_generic_type.h"
1313
#include <util/namespace.h>
14-
#include <util/prefix.h>
1514
#include <java_bytecode/java_types.h>
1615
#include <java_bytecode/java_utils.h>
1716

18-
/// Strip the package name from a java type, for the type to be
19-
/// pretty printed (java::java.lang.Integer -> Integer).
20-
/// \param fqn_java_type The java type we want to pretty print.
21-
/// \return The pretty printed type if there was a match of the
22-
// qualifiers, or the type as it was passed otherwise.
23-
std::string pretty_print_java_type(const std::string &fqn_java_type)
24-
{
25-
std::string result(fqn_java_type);
26-
const std::string java_cbmc_string("java::");
27-
// Remove the java internal cbmc identifier
28-
if(has_prefix(fqn_java_type, java_cbmc_string))
29-
result = fqn_java_type.substr(java_cbmc_string.length());
30-
// If the class is in package java.lang strip
31-
// package name due to default import
32-
const std::string java_lang_string("java.lang.");
33-
if(has_prefix(result, java_lang_string))
34-
result = result.substr(java_lang_string.length());
35-
return result;
36-
}
37-
3817
generate_java_generic_typet::generate_java_generic_typet(
3918
message_handlert &message_handler):
4019
message_handler(message_handler)

src/java_bytecode/generate_java_generic_type.h

-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,4 @@ class generate_java_generic_typet
4343
message_handlert &message_handler;
4444
};
4545

46-
std::string pretty_print_java_type(const std::string &fqn_java_type);
47-
4846
#endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H

src/java_bytecode/java_utils.cpp

+20
Original file line numberDiff line numberDiff line change
@@ -305,3 +305,23 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
305305
PRECONDITION(has_prefix(to_strip_str, prefix));
306306
return to_strip_str.substr(prefix.size(), std::string::npos);
307307
}
308+
309+
/// Strip the package name from a java type, for the type to be
310+
/// pretty printed (java::java.lang.Integer -> Integer).
311+
/// \param fqn_java_type The java type we want to pretty print.
312+
/// \return The pretty printed type if there was a match of the
313+
// qualifiers, or the type as it was passed otherwise.
314+
std::string pretty_print_java_type(const std::string &fqn_java_type)
315+
{
316+
std::string result(fqn_java_type);
317+
const std::string java_cbmc_string("java::");
318+
// Remove the CBMC internal java identifier
319+
if(has_prefix(fqn_java_type, java_cbmc_string))
320+
result = fqn_java_type.substr(java_cbmc_string.length());
321+
// If the class is in package java.lang strip
322+
// package name due to default import
323+
const std::string java_lang_string("java.lang.");
324+
if(has_prefix(result, java_lang_string))
325+
result = result.substr(java_lang_string.length());
326+
return result;
327+
}

src/java_bytecode/java_utils.h

+2
Original file line numberDiff line numberDiff line change
@@ -94,4 +94,6 @@ exprt make_function_application(
9494

9595
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip);
9696

97+
std::string pretty_print_java_type(const std::string &fqn_java_type);
98+
9799
#endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

-29
Original file line numberDiff line numberDiff line change
@@ -392,32 +392,3 @@ SCENARIO(
392392
}
393393
}
394394
}
395-
396-
SCENARIO(
397-
"Test pretty printing auxiliary function",
398-
"[core][java_bytecode][generate_java_generic_type]")
399-
{
400-
using std::map;
401-
using std::string;
402-
403-
WHEN("We have a series of cbmc internal java types")
404-
{
405-
// NOLINTNEXTLINE
406-
const map<string, string> types{
407-
// map<Input, Output>
408-
{"java::java.lang.Integer", "Integer"},
409-
{"java::CustomClass", "CustomClass"},
410-
{"java.lang.String", "String"},
411-
{"Hashmap", "Hashmap"},
412-
// We shouldn't prune types not imported in default import
413-
{"java.util.HashSet", "java.util.HashSet"}};
414-
415-
THEN("We need to make sure that the types get pruned correctly.")
416-
{
417-
for(const auto &pair : types)
418-
{
419-
REQUIRE(pretty_print_java_type(pair.first) == pair.second);
420-
}
421-
}
422-
}
423-
}

unit/java_bytecode/java_utils_test.cpp

+27
Original file line numberDiff line numberDiff line change
@@ -341,3 +341,30 @@ SCENARIO("find_closing_semi_colon_for_reference_type", "[core][java_util_test]")
341341
REQUIRE(find_closing_semi_colon_for_reference_type(descriptor, 10) == 19);
342342
}
343343
}
344+
345+
SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]")
346+
{
347+
using std::map;
348+
using std::string;
349+
350+
WHEN("We have a series of cbmc internal java types")
351+
{
352+
// NOLINTNEXTLINE
353+
const map<string, string> types{
354+
// map<Input, Output>
355+
{"java::java.lang.Integer", "Integer"},
356+
{"java::CustomClass", "CustomClass"},
357+
{"java.lang.String", "String"},
358+
{"Hashmap", "Hashmap"},
359+
// We shouldn't prune types not imported in default import
360+
{"java.util.HashSet", "java.util.HashSet"}};
361+
362+
THEN("We need to make sure that the types get pruned correctly.")
363+
{
364+
for(const auto &pair : types)
365+
{
366+
REQUIRE(pretty_print_java_type(pair.first) == pair.second);
367+
}
368+
}
369+
}
370+
}

0 commit comments

Comments
 (0)