|
3 | 3 | Module: Unit tests for dependency graph
|
4 | 4 | solvers/refinement/string_refinement.cpp
|
5 | 5 |
|
6 |
| - Author: DiffBlue Limited. All rights reserved. |
| 6 | + Author: DiffBlue Ltd. |
7 | 7 |
|
8 | 8 | \*******************************************************************/
|
9 | 9 |
|
@@ -47,7 +47,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
|
47 | 47 | {
|
48 | 48 | GIVEN("dependency graph")
|
49 | 49 | {
|
50 |
| - string_dependenciest dependences; |
| 50 | + string_dependenciest dependencies; |
51 | 51 | refined_string_typet string_type(java_char_type(), java_int_type());
|
52 | 52 | const exprt string1 = make_string_argument("string1");
|
53 | 53 | const exprt string2 = make_string_argument("string2");
|
@@ -93,21 +93,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
|
93 | 93 | symbol_generatort generator;
|
94 | 94 | array_poolt array_pool(generator);
|
95 | 95 |
|
96 |
| - bool success = add_node(dependences, equation1, array_pool); |
| 96 | + bool success = add_node(dependencies, equation1, array_pool); |
97 | 97 | REQUIRE(success);
|
98 |
| - success = add_node(dependences, equation2, array_pool); |
| 98 | + success = add_node(dependencies, equation2, array_pool); |
99 | 99 | REQUIRE(success);
|
100 |
| - success = add_node(dependences, equation3, array_pool); |
| 100 | + success = add_node(dependencies, equation3, array_pool); |
101 | 101 | REQUIRE(success);
|
102 | 102 |
|
103 | 103 | #ifdef DEBUG // useful output for visualizing the graph
|
104 | 104 | {
|
105 | 105 | register_language(new_java_bytecode_language);
|
106 | 106 | symbol_tablet symbol_table;
|
107 | 107 | namespacet ns(symbol_table);
|
108 |
| - dependencies.output_dot(std::cerr, [&](const exprt &expr) { // NOLINT |
109 |
| - return from_expr(ns, "", expr); |
110 |
| - }); |
| 108 | + dependencies.output_dot(std::cerr); |
111 | 109 | }
|
112 | 110 | #endif
|
113 | 111 |
|
@@ -141,53 +139,56 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
|
141 | 139 |
|
142 | 140 | THEN("string3 depends on primitive0")
|
143 | 141 | {
|
144 |
| - const auto &node = dependences.get_node(char_array3); |
145 |
| - const std::vector<string_dependenciest::builtin_function_nodet> |
146 |
| - &depends = dependences.dependencies(node); |
147 |
| - REQUIRE(depends.size() == 1); |
148 |
| - const auto &primitive0 = dependences.get_builtin_function(depends[0]); |
149 |
| - |
150 |
| - THEN("primitive0 depends on string1 and string2") |
151 |
| - { |
152 |
| - const auto &depends2 = primitive0.string_arguments(); |
153 |
| - REQUIRE(depends2.size() == 2); |
154 |
| - REQUIRE(depends2[0] == char_array1); |
155 |
| - REQUIRE(depends2[1] == char_array2); |
156 |
| - } |
| 142 | + const auto &node = dependencies.get_node(char_array3); |
| 143 | + std::size_t nb_dependencies = 0; |
| 144 | + dependencies.for_each_dependency( |
| 145 | + node, [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT |
| 146 | + nb_dependencies++; |
| 147 | + THEN("primitive0 depends on string1 and string2") |
| 148 | + { |
| 149 | + const auto &depends2 = n.data->string_arguments(); |
| 150 | + REQUIRE(depends2.size() == 2); |
| 151 | + REQUIRE(depends2[0] == char_array1); |
| 152 | + REQUIRE(depends2[1] == char_array2); |
| 153 | + } |
| 154 | + }); |
| 155 | + REQUIRE(nb_dependencies == 1); |
157 | 156 | }
|
158 | 157 |
|
159 | 158 | THEN("string5 depends on primitive1")
|
160 | 159 | {
|
161 |
| - const auto &node = dependences.get_node(char_array5); |
162 |
| - const std::vector<string_dependenciest::builtin_function_nodet> |
163 |
| - &depends = dependences.dependencies(node); |
164 |
| - REQUIRE(depends.size() == 1); |
165 |
| - const auto &primitive1 = dependences.get_builtin_function(depends[0]); |
166 |
| - |
167 |
| - THEN("primitive1 depends on string3 and string4") |
168 |
| - { |
169 |
| - const auto &depends2 = primitive1.string_arguments(); |
170 |
| - REQUIRE(depends2.size() == 2); |
171 |
| - REQUIRE(depends2[0] == char_array3); |
172 |
| - REQUIRE(depends2[1] == char_array4); |
173 |
| - } |
| 160 | + const auto &node = dependencies.get_node(char_array5); |
| 161 | + std::size_t nb_dependencies = 0; |
| 162 | + dependencies.for_each_dependency( |
| 163 | + node, [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT |
| 164 | + nb_dependencies++; |
| 165 | + THEN("primitive1 depends on string3 and string4") |
| 166 | + { |
| 167 | + const auto &depends2 = n.data->string_arguments(); |
| 168 | + REQUIRE(depends2.size() == 2); |
| 169 | + REQUIRE(depends2[0] == char_array3); |
| 170 | + REQUIRE(depends2[1] == char_array4); |
| 171 | + } |
| 172 | + }); |
| 173 | + REQUIRE(nb_dependencies == 1); |
174 | 174 | }
|
175 | 175 |
|
176 | 176 | THEN("string6 depends on primitive2")
|
177 | 177 | {
|
178 |
| - const auto &node = dependences.get_node(char_array6); |
179 |
| - const std::vector<string_dependenciest::builtin_function_nodet> |
180 |
| - &depends = dependences.dependencies(node); |
181 |
| - REQUIRE(depends.size() == 1); |
182 |
| - const auto &primitive2 = dependences.get_builtin_function(depends[0]); |
183 |
| - |
184 |
| - THEN("primitive2 depends on string5 and string2") |
185 |
| - { |
186 |
| - const auto &depends2 = primitive2.string_arguments(); |
187 |
| - REQUIRE(depends2.size() == 2); |
188 |
| - REQUIRE(depends2[0] == char_array5); |
189 |
| - REQUIRE(depends2[1] == char_array2); |
190 |
| - } |
| 178 | + const auto &node = dependencies.get_node(char_array6); |
| 179 | + std::size_t nb_dependencies = 0; |
| 180 | + dependencies.for_each_dependency( |
| 181 | + node, [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT |
| 182 | + nb_dependencies++; |
| 183 | + THEN("primitive2 depends on string5 and string2") |
| 184 | + { |
| 185 | + const auto &depends2 = n.data->string_arguments(); |
| 186 | + REQUIRE(depends2.size() == 2); |
| 187 | + REQUIRE(depends2[0] == char_array5); |
| 188 | + REQUIRE(depends2[1] == char_array2); |
| 189 | + } |
| 190 | + }); |
| 191 | + REQUIRE(nb_dependencies == 1); |
191 | 192 | }
|
192 | 193 | }
|
193 | 194 | }
|
|
0 commit comments