6
6
7
7
\*******************************************************************/
8
8
9
- #include < goto-programs/goto_program.h>
10
9
#include " java_testing_utils.h"
11
10
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>
27
13
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;
29
43
}
30
44
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 ,
33
47
const irep_idt &structure_name,
34
48
const irep_idt &component_name)
35
49
{
36
- struct_component_assignment_locationt component_assignments;
50
+ std::vector<code_assignt> component_assignments;
37
51
38
- for (const auto &instruction : entry_point_instructions )
52
+ for (const auto &assignment : statements )
39
53
{
40
- const codet &assignment = to_code (instruction);
41
- INVARIANT (instruction.id () == ID_code, " All instructions must be code" );
42
54
if (assignment.get_statement () == ID_assign)
43
55
{
44
56
const code_assignt &code_assign = to_code_assign (assignment);
@@ -52,105 +64,29 @@ struct_component_assignment_locationt find_struct_component_assignments(
52
64
symbol.get_identifier () == structure_name &&
53
65
member_expr.get_component_name () == component_name)
54
66
{
55
- component_assignments.assignment_locations . push_back (code_assign);
67
+ component_assignments.push_back (code_assign);
56
68
}
57
69
}
58
70
}
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
- }
97
71
}
98
72
return component_assignments;
99
73
}
100
74
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
-
137
75
// / For a given variable name, gets the assignments to it in the functions
138
76
// / \param pointer_name: The name of the variable
139
77
// / \param instructions: The instructions to look through
140
78
// / \return: A structure that contains the null assignment if found, and a
141
79
// / vector of all other assignments
142
80
pointer_assignment_locationt find_pointer_assignments (
143
81
const irep_idt &pointer_name,
144
- const exprt::operandst &instructions)
82
+ const std::vector<codet> &instructions)
145
83
{
146
84
pointer_assignment_locationt locations;
147
- for (const exprt &assignment : instructions)
85
+ for (const codet &statement : instructions)
148
86
{
149
- const codet &statement = to_code (assignment);
150
- INVARIANT (assignment.id () == ID_code, " All instructions must be code" );
151
87
if (statement.get_statement () == ID_assign)
152
88
{
153
- const code_assignt &code_assign = to_code_assign (to_code (assignment) );
89
+ const code_assignt &code_assign = to_code_assign (statement );
154
90
if (
155
91
code_assign.lhs ().id () == ID_symbol &&
156
92
to_symbol_expr (code_assign.lhs ()).get_identifier () == pointer_name)
@@ -167,56 +103,26 @@ pointer_assignment_locationt find_pointer_assignments(
167
103
}
168
104
}
169
105
}
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
- }
198
106
}
199
107
200
108
return locations;
201
109
}
202
110
203
111
const exprt &find_declaration_by_name (
204
112
const irep_idt &variable_name,
205
- const exprt::operandst &entry_point_instructions)
113
+ const std::vector<codet> &entry_point_instructions)
206
114
{
207
- for (const auto &instruction : entry_point_instructions)
115
+ for (const auto &statement : entry_point_instructions)
208
116
{
209
- const codet &statement = to_code (instruction);
210
- INVARIANT (instruction.id () == ID_code, " All instructions must be code" );
211
117
if (statement.get_statement () == ID_decl)
212
118
{
213
119
const auto &decl_statement = to_code_decl (statement);
214
120
215
121
if (decl_statement.get_identifier () == variable_name)
216
122
{
217
- return instruction ;
123
+ return statement ;
218
124
}
219
125
}
220
126
}
221
127
throw no_decl_found_exception (variable_name.c_str ());
222
- }
128
+ }
0 commit comments