66
77\*******************************************************************/
88
9- #include < goto-programs/goto_program.h>
109#include " java_testing_utils.h"
1110
12- struct_component_assignment_locationt combine_locations (
13- const struct_component_assignment_locationt &a,
14- const struct_component_assignment_locationt &b)
15- {
16- struct_component_assignment_locationt new_locations;
17-
18- new_locations.assignment_locations .insert (
19- new_locations.assignment_locations .end (),
20- a.assignment_locations .begin (),
21- a.assignment_locations .end ());
22-
23- new_locations.assignment_locations .insert (
24- new_locations.assignment_locations .end (),
25- b.assignment_locations .begin (),
26- b.assignment_locations .end ());
11+ #include < algorithm>
12+ #include < util/expr_iterator.h>
2713
28- return new_locations;
14+ std::vector<codet> get_all_statements (const exprt::operandst &instructions)
15+ {
16+ std::vector<codet> statements;
17+ for (const exprt &instruction : instructions)
18+ {
19+ // Add the statement
20+ statements.push_back (to_code (instruction));
21+
22+ // Add any child statements (e.g. if this is a code_block
23+ // TODO(tkiley): It should be possible to have a custom version of
24+ // TODO(tkiley): back_inserter that also transforms to codet, but I don't
25+ // TODO(tkiley): know how to do this
26+ std::vector<exprt> sub_expr;
27+ std::copy_if (
28+ instruction.depth_begin (),
29+ instruction.depth_end (),
30+ std::back_inserter (sub_expr),
31+ [](const exprt &sub_statement) {
32+ // Get all codet
33+ return sub_statement.id () == ID_code;
34+ });
35+
36+ std::transform (
37+ sub_expr.begin (),
38+ sub_expr.end (),
39+ std::back_inserter (statements),
40+ [](const exprt &sub_expr) { return to_code (sub_expr); });
41+ }
42+ return statements;
2943}
3044
31- struct_component_assignment_locationt find_struct_component_assignments (
32- const exprt::operandst &entry_point_instructions ,
45+ std::vector<code_assignt> find_struct_component_assignments (
46+ const std::vector<codet> &statements ,
3347 const irep_idt &structure_name,
3448 const irep_idt &component_name)
3549{
36- struct_component_assignment_locationt component_assignments;
50+ std::vector<code_assignt> component_assignments;
3751
38- for (const auto &instruction : entry_point_instructions )
52+ for (const auto &assignment : statements )
3953 {
40- const codet &assignment = to_code (instruction);
41- INVARIANT (instruction.id () == ID_code, " All instructions must be code" );
4254 if (assignment.get_statement () == ID_assign)
4355 {
4456 const code_assignt &code_assign = to_code_assign (assignment);
@@ -52,105 +64,29 @@ struct_component_assignment_locationt find_struct_component_assignments(
5264 symbol.get_identifier () == structure_name &&
5365 member_expr.get_component_name () == component_name)
5466 {
55- component_assignments.assignment_locations . push_back (code_assign);
67+ component_assignments.push_back (code_assign);
5668 }
5769 }
5870 }
59- else if (assignment.get_statement () == ID_block)
60- {
61- const auto &assignments_in_block = find_struct_component_assignments (
62- assignment.operands (), structure_name, component_name);
63- component_assignments =
64- combine_locations (component_assignments, assignments_in_block);
65- }
66- else if (assignment.get_statement () == ID_ifthenelse)
67- {
68- const code_ifthenelset &if_else_block =
69- to_code_ifthenelse (to_code (assignment));
70- const auto &assignments_in_block = find_struct_component_assignments (
71- exprt::operandst{if_else_block.then_case ()},
72- structure_name,
73- component_name);
74- component_assignments =
75- combine_locations (component_assignments, assignments_in_block);
76-
77- if (if_else_block.has_else_case ())
78- {
79- const auto &assignments_in_else = find_struct_component_assignments (
80- exprt::operandst{if_else_block.else_case ()},
81- structure_name,
82- component_name);
83- component_assignments =
84- combine_locations (component_assignments, assignments_in_else);
85- }
86- }
87- else if (assignment.get_statement () == ID_label)
88- {
89- const code_labelt &label_statement = to_code_label (assignment);
90- const auto &assignments_in_label = find_struct_component_assignments (
91- exprt::operandst{label_statement.code ()},
92- structure_name,
93- component_name);
94- component_assignments =
95- combine_locations (component_assignments, assignments_in_label);
96- }
9771 }
9872 return component_assignments;
9973}
10074
101- // / Combine two pointer locations. Takes the null assignment if present in
102- // / either (fails if present in both) and appends the non-null assignments
103- // / \param a: The first set of assignments
104- // / \param b: The second set of assignments
105- // / \return The resulting assignment
106- pointer_assignment_locationt combine_locations (
107- const pointer_assignment_locationt &a,
108- const pointer_assignment_locationt &b)
109- {
110- pointer_assignment_locationt new_locations;
111- if (a.null_assignment .has_value ())
112- {
113- INVARIANT (
114- !b.null_assignment .has_value (), " Only expected one assignment to null" );
115- new_locations.null_assignment = a.null_assignment ;
116- }
117- else if (b.null_assignment .has_value ())
118- {
119- INVARIANT (
120- !a.null_assignment .has_value (), " Only expected one assignment to null" );
121- new_locations.null_assignment = b.null_assignment ;
122- }
123-
124- new_locations.non_null_assignments .insert (
125- new_locations.non_null_assignments .end (),
126- a.non_null_assignments .begin (),
127- a.non_null_assignments .end ());
128-
129- new_locations.non_null_assignments .insert (
130- new_locations.non_null_assignments .end (),
131- b.non_null_assignments .begin (),
132- b.non_null_assignments .end ());
133-
134- return new_locations;
135- }
136-
13775// / For a given variable name, gets the assignments to it in the functions
13876// / \param pointer_name: The name of the variable
13977// / \param instructions: The instructions to look through
14078// / \return: A structure that contains the null assignment if found, and a
14179// / vector of all other assignments
14280pointer_assignment_locationt find_pointer_assignments (
14381 const irep_idt &pointer_name,
144- const exprt::operandst &instructions)
82+ const std::vector<codet> &instructions)
14583{
14684 pointer_assignment_locationt locations;
147- for (const exprt &assignment : instructions)
85+ for (const codet &statement : instructions)
14886 {
149- const codet &statement = to_code (assignment);
150- INVARIANT (assignment.id () == ID_code, " All instructions must be code" );
15187 if (statement.get_statement () == ID_assign)
15288 {
153- const code_assignt &code_assign = to_code_assign (to_code (assignment) );
89+ const code_assignt &code_assign = to_code_assign (statement );
15490 if (
15591 code_assign.lhs ().id () == ID_symbol &&
15692 to_symbol_expr (code_assign.lhs ()).get_identifier () == pointer_name)
@@ -167,56 +103,26 @@ pointer_assignment_locationt find_pointer_assignments(
167103 }
168104 }
169105 }
170- else if (statement.get_statement () == ID_block)
171- {
172- const auto &assignments_in_block =
173- find_pointer_assignments (pointer_name, assignment.operands ());
174- locations = combine_locations (locations, assignments_in_block);
175- }
176- else if (statement.get_statement () == ID_ifthenelse)
177- {
178- const code_ifthenelset &if_else_block =
179- to_code_ifthenelse (to_code (assignment));
180- const auto &assignments_in_block = find_pointer_assignments (
181- pointer_name, exprt::operandst{if_else_block.then_case ()});
182- locations = combine_locations (locations, assignments_in_block);
183-
184- if (if_else_block.has_else_case ())
185- {
186- const auto &assignments_in_else = find_pointer_assignments (
187- pointer_name, exprt::operandst{if_else_block.else_case ()});
188- locations = combine_locations (locations, assignments_in_else);
189- }
190- }
191- else if (statement.get_statement () == ID_label)
192- {
193- const code_labelt &label_statement = to_code_label (statement);
194- const auto &assignments_in_label = find_pointer_assignments (
195- pointer_name, exprt::operandst{label_statement.code ()});
196- locations = combine_locations (locations, assignments_in_label);
197- }
198106 }
199107
200108 return locations;
201109}
202110
203111const exprt &find_declaration_by_name (
204112 const irep_idt &variable_name,
205- const exprt::operandst &entry_point_instructions)
113+ const std::vector<codet> &entry_point_instructions)
206114{
207- for (const auto &instruction : entry_point_instructions)
115+ for (const auto &statement : entry_point_instructions)
208116 {
209- const codet &statement = to_code (instruction);
210- INVARIANT (instruction.id () == ID_code, " All instructions must be code" );
211117 if (statement.get_statement () == ID_decl)
212118 {
213119 const auto &decl_statement = to_code_decl (statement);
214120
215121 if (decl_statement.get_identifier () == variable_name)
216122 {
217- return instruction ;
123+ return statement ;
218124 }
219125 }
220126 }
221127 throw no_decl_found_exception (variable_name.c_str ());
222- }
128+ }
0 commit comments