File: class_hierarchy_graph.cpp

package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36
file content (136 lines) | stat: -rw-r--r-- 4,444 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
/*******************************************************************\

Module: Unit tests for class_hierarchy_grapht

Author: Diffblue Ltd.

\*******************************************************************/

#include <java-testing-utils/load_java_class.h>
#include <testing-utils/use_catch.h>

#include <goto-programs/class_hierarchy.h>

void require_parent_child_relationship(
  const std::string &parent_raw,
  const std::string &child_raw,
  const class_hierarchy_grapht &hierarchy)
{
  irep_idt parent = "java::" + parent_raw;
  irep_idt child = "java::" + child_raw;

  const class_hierarchy_grapht::nodes_by_namet &nodes_map =
    hierarchy.get_nodes_by_class_identifier();
  REQUIRE(nodes_map.count(parent) != 0);
  REQUIRE(nodes_map.count(child) != 0);
  REQUIRE(hierarchy.has_edge(nodes_map.at(parent), nodes_map.at(child)));
}

SCENARIO(
  "Output a simple class hierarchy graph",
  "[core][goto-programs][class_hierarchy_graph]")
{
  symbol_tablet symbol_table =
    load_java_class("HierarchyTest", "./java_bytecode/goto-programs/");
  class_hierarchy_grapht hierarchy;
  hierarchy.populate(symbol_table);

  require_parent_child_relationship(
    "HierarchyTest", "HierarchyTestChild1", hierarchy);
  require_parent_child_relationship(
    "HierarchyTest", "HierarchyTestChild2", hierarchy);
  require_parent_child_relationship(
    "HierarchyTestChild1", "HierarchyTestGrandchild", hierarchy);
  require_parent_child_relationship(
    "HierarchyTestInterface1", "HierarchyTestGrandchild", hierarchy);
  require_parent_child_relationship(
    "HierarchyTestInterface2", "HierarchyTestGrandchild", hierarchy);
}

SCENARIO(
  "class_hierarchy_graph",
  "[core][goto-programs][class_hierarchy_graph]")
{
  symbol_tablet symbol_table =
    load_java_class("HierarchyTest", "./java_bytecode/goto-programs/");
  class_hierarchy_grapht hierarchy;
  hierarchy.populate(symbol_table);

  WHEN("Retrieving direct children of a given class")
  {
    const class_hierarchy_grapht::idst ht_direct_children =
      hierarchy.get_direct_children("java::HierarchyTest");
    THEN("The correct list of direct children should be returned")
    {
      REQUIRE(ht_direct_children.size() == 2);
      REQUIRE(
        find(
          ht_direct_children.begin(),
          ht_direct_children.end(),
          "java::HierarchyTestChild1") != ht_direct_children.end());
      REQUIRE(
        find(
          ht_direct_children.begin(),
          ht_direct_children.end(),
          "java::HierarchyTestChild2") != ht_direct_children.end());
    }
  }
  WHEN("Retrieving all children of a given class")
  {
    const class_hierarchy_grapht::idst ht_all_children =
      hierarchy.get_children_trans("java::HierarchyTest");
    THEN("The correct list of children should be returned")
    {
      REQUIRE(ht_all_children.size() == 3);
      REQUIRE(
        find(
          ht_all_children.begin(),
          ht_all_children.end(),
          "java::HierarchyTestChild1") != ht_all_children.end());
      REQUIRE(
        find(
          ht_all_children.begin(),
          ht_all_children.end(),
          "java::HierarchyTestChild2") != ht_all_children.end());
      REQUIRE(
        find(
          ht_all_children.begin(),
          ht_all_children.end(),
          "java::HierarchyTestGrandchild") != ht_all_children.end());
    }
  }
  WHEN("Retrieving all parents of a given class")
  {
    const class_hierarchy_grapht::idst htg_all_parents =
      hierarchy.get_parents_trans("java::HierarchyTestGrandchild");
    THEN("The correct list of parents should be returned")
    {
      REQUIRE(htg_all_parents.size() == 5);
      REQUIRE(
        find(
          htg_all_parents.begin(),
          htg_all_parents.end(),
          "java::HierarchyTestChild1") != htg_all_parents.end());
      REQUIRE(
        find(
          htg_all_parents.begin(),
          htg_all_parents.end(),
          "java::HierarchyTest") != htg_all_parents.end());
      REQUIRE(
        find(
          htg_all_parents.begin(),
          htg_all_parents.end(),
          "java::HierarchyTestInterface1") != htg_all_parents.end());
      REQUIRE(
        find(
          htg_all_parents.begin(),
          htg_all_parents.end(),
          "java::HierarchyTestInterface2") != htg_all_parents.end());
      REQUIRE(
        find(
          htg_all_parents.begin(),
          htg_all_parents.end(),
          "java::java.lang.Object") != htg_all_parents.end());
    }
  }
}