Skip to content

Commit 61e4d58

Browse files
committed
Add checks of get_name() to inner class unit test
1 parent 2dcbb00 commit 61e4d58

File tree

1 file changed

+16
-0
lines changed

1 file changed

+16
-0
lines changed

jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,10 @@ SCENARIO(
2626
type_try_dynamic_cast<java_class_typet>(class_symbol->type);
2727
REQUIRE(class_type);
2828

29+
THEN("The inner class should have the name \"java::Outer$Inner\".")
30+
{
31+
REQUIRE(id2string(class_type->get_name()) == "java::Outer$Inner");
32+
}
2933
THEN("The inner class should have the inner name \"Inner\".")
3034
{
3135
REQUIRE(id2string(class_type->get_inner_name()) == "Inner");
@@ -52,6 +56,10 @@ SCENARIO(
5256
type_try_dynamic_cast<java_class_typet>(class_symbol->type);
5357
REQUIRE(class_type);
5458

59+
THEN("The outer class should have the name \"java::Outer\".")
60+
{
61+
REQUIRE(id2string(class_type->get_name()) == "java::Outer");
62+
}
5563
THEN("The outer class should not have an inner name.")
5664
{
5765
REQUIRE(id2string(class_type->get_inner_name()).empty());
@@ -78,6 +86,10 @@ SCENARIO(
7886
type_try_dynamic_cast<java_class_typet>(class_symbol->type);
7987
REQUIRE(class_type);
8088

89+
THEN("The anonymous class should have the name \"java::Outer$1\".")
90+
{
91+
REQUIRE(id2string(class_type->get_name()) == "java::Outer$1");
92+
}
8193
THEN("The anonymous class should not have an inner name.")
8294
{
8395
REQUIRE(id2string(class_type->get_inner_name()).empty());
@@ -104,6 +116,10 @@ SCENARIO(
104116
type_try_dynamic_cast<java_class_typet>(class_symbol->type);
105117
REQUIRE(class_type);
106118

119+
THEN("The outer class should have the name \"java::Outer$RedHerring\".")
120+
{
121+
REQUIRE(id2string(class_type->get_name()) == "java::Outer$RedHerring");
122+
}
107123
THEN("The outer class should not have an inner name.")
108124
{
109125
REQUIRE(id2string(class_type->get_inner_name()).empty());

0 commit comments

Comments
 (0)