@@ -153,28 +153,42 @@ require_goto_statements::find_pointer_assignments(
153
153
const std::vector<codet> &instructions)
154
154
{
155
155
pointer_assignment_locationt locations;
156
+ bool found_assignment = false ;
157
+ std::vector<irep_idt> all_symbols;
156
158
for (const codet &statement : instructions)
157
159
{
158
160
if (statement.get_statement () == ID_assign)
159
161
{
160
162
const code_assignt &code_assign = to_code_assign (statement);
161
- if (
162
- code_assign.lhs ().id () == ID_symbol &&
163
- to_symbol_expr (code_assign.lhs ()).get_identifier () == pointer_name)
163
+ if (code_assign.lhs ().id () == ID_symbol)
164
164
{
165
- if (
166
- code_assign. rhs () ==
167
- null_pointer_exprt ( to_pointer_type (code_assign. lhs (). type ())) )
165
+ const symbol_exprt &symbol_expr = to_symbol_expr (code_assign. lhs ());
166
+ all_symbols. push_back (symbol_expr. get_identifier ());
167
+ if (symbol_expr. get_identifier () == pointer_name )
168
168
{
169
- locations.null_assignment = code_assign;
170
- }
171
- else
172
- {
173
- locations.non_null_assignments .push_back (code_assign);
169
+ if (
170
+ code_assign.rhs () ==
171
+ null_pointer_exprt (to_pointer_type (code_assign.lhs ().type ())))
172
+ {
173
+ locations.null_assignment = code_assign;
174
+ }
175
+ else
176
+ {
177
+ locations.non_null_assignments .push_back (code_assign);
178
+ }
179
+ found_assignment = true ;
174
180
}
175
181
}
176
182
}
177
183
}
184
+ INFO (" Looking for symbol: " << pointer_name);
185
+ std::ostringstream found_symbols;
186
+ for (const auto entry : all_symbols)
187
+ {
188
+ found_symbols << entry << std::endl;
189
+ }
190
+ INFO (" Symbols: " << found_symbols.str ());
191
+ REQUIRE (found_assignment);
178
192
179
193
return locations;
180
194
}
0 commit comments