Skip to content

Commit ff7b37c

Browse files
committed
Add tests for new class_hierarchy_grapht functions
1 parent 75000c0 commit ff7b37c

File tree

1 file changed

+88
-0
lines changed

1 file changed

+88
-0
lines changed

jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp

+88
Original file line numberDiff line numberDiff line change
@@ -46,3 +46,91 @@ SCENARIO(
4646
require_parent_child_relationship(
4747
"HierarchyTestInterface2", "HierarchyTestGrandchild", hierarchy);
4848
}
49+
50+
SCENARIO(
51+
"class_hierarchy_graph",
52+
"[core][goto-programs][class_hierarchy_graph]")
53+
{
54+
symbol_tablet symbol_table =
55+
load_java_class("HierarchyTest", "./java_bytecode/goto-programs/");
56+
class_hierarchy_grapht hierarchy;
57+
hierarchy.populate(symbol_table);
58+
59+
WHEN("Retrieving direct children of a given class")
60+
{
61+
const class_hierarchy_grapht::idst ht_direct_children =
62+
hierarchy.get_direct_children("java::HierarchyTest");
63+
THEN("The correct list of direct children should be returned")
64+
{
65+
REQUIRE(ht_direct_children.size() == 2);
66+
REQUIRE(
67+
find(
68+
ht_direct_children.begin(),
69+
ht_direct_children.end(),
70+
"java::HierarchyTestChild1") != ht_direct_children.end());
71+
REQUIRE(
72+
find(
73+
ht_direct_children.begin(),
74+
ht_direct_children.end(),
75+
"java::HierarchyTestChild2") != ht_direct_children.end());
76+
}
77+
}
78+
WHEN("Retrieving all children of a given class")
79+
{
80+
const class_hierarchy_grapht::idst ht_all_children =
81+
hierarchy.get_children_trans("java::HierarchyTest");
82+
THEN("The correct list of children should be returned")
83+
{
84+
REQUIRE(ht_all_children.size() == 3);
85+
REQUIRE(
86+
find(
87+
ht_all_children.begin(),
88+
ht_all_children.end(),
89+
"java::HierarchyTestChild1") != ht_all_children.end());
90+
REQUIRE(
91+
find(
92+
ht_all_children.begin(),
93+
ht_all_children.end(),
94+
"java::HierarchyTestChild2") != ht_all_children.end());
95+
REQUIRE(
96+
find(
97+
ht_all_children.begin(),
98+
ht_all_children.end(),
99+
"java::HierarchyTestGrandchild") != ht_all_children.end());
100+
}
101+
}
102+
WHEN("Retrieving all parents of a given class")
103+
{
104+
const class_hierarchy_grapht::idst htg_all_parents =
105+
hierarchy.get_parents_trans("java::HierarchyTestGrandchild");
106+
THEN("The correct list of parents should be returned")
107+
{
108+
REQUIRE(htg_all_parents.size() == 5);
109+
REQUIRE(
110+
find(
111+
htg_all_parents.begin(),
112+
htg_all_parents.end(),
113+
"java::HierarchyTestChild1") != htg_all_parents.end());
114+
REQUIRE(
115+
find(
116+
htg_all_parents.begin(),
117+
htg_all_parents.end(),
118+
"java::HierarchyTest") != htg_all_parents.end());
119+
REQUIRE(
120+
find(
121+
htg_all_parents.begin(),
122+
htg_all_parents.end(),
123+
"java::HierarchyTestInterface1") != htg_all_parents.end());
124+
REQUIRE(
125+
find(
126+
htg_all_parents.begin(),
127+
htg_all_parents.end(),
128+
"java::HierarchyTestInterface2") != htg_all_parents.end());
129+
REQUIRE(
130+
find(
131+
htg_all_parents.begin(),
132+
htg_all_parents.end(),
133+
"java::java.lang.Object") != htg_all_parents.end());
134+
}
135+
}
136+
}

0 commit comments

Comments
 (0)