@@ -198,51 +198,6 @@ void restrict_function_pointer(
198
198
address_of_exprt{function_pointer_target_symbol_expr}}));
199
199
}
200
200
}
201
-
202
- void get_by_name_restriction (
203
- const goto_functiont &goto_function,
204
- const function_pointer_restrictionst::restrictionst &by_name_restrictions,
205
- function_pointer_restrictionst::restrictionst &restrictions,
206
- const goto_programt::const_targett &location)
207
- {
208
- PRECONDITION (location->is_function_call ());
209
-
210
- const exprt &function = location->get_function_call ().function ();
211
-
212
- if (!can_cast_expr<dereference_exprt>(function))
213
- return ;
214
-
215
- auto const &function_pointer_call_site = to_symbol_expr (
216
- to_dereference_expr (function)
217
- .pointer ());
218
-
219
- for (auto it = std::prev (location);
220
- it != goto_function.body .instructions .end ();
221
- ++it)
222
- {
223
- if (!it->is_assign ())
224
- continue ;
225
-
226
- if (it->get_assign ().lhs () != function_pointer_call_site)
227
- continue ;
228
-
229
- if (!can_cast_expr<symbol_exprt>(it->get_assign ().rhs ()))
230
- continue ;
231
-
232
- auto const &rhs = to_symbol_expr (it->get_assign ().rhs ());
233
- auto const restriction =
234
- by_name_restrictions.find (rhs.get_identifier ());
235
-
236
- if (
237
- restriction != by_name_restrictions.end () &&
238
- restriction->first == rhs.get_identifier ())
239
- {
240
- restrictions.emplace (
241
- function_pointer_call_site.get_identifier (),
242
- restriction->second );
243
- }
244
- }
245
- }
246
201
} // namespace
247
202
248
203
void restrict_function_pointers (
@@ -431,6 +386,49 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
431
386
return std::make_pair (pointer_name, target_names);
432
387
}
433
388
389
+ optionalt<function_pointer_restrictionst::restrictiont>
390
+ function_pointer_restrictionst::get_by_name_restriction (
391
+ const goto_functiont &goto_function,
392
+ const function_pointer_restrictionst::restrictionst &by_name_restrictions,
393
+ const goto_programt::const_targett &location)
394
+ {
395
+ PRECONDITION (location->is_function_call ());
396
+
397
+ const exprt &function = location->get_function_call ().function ();
398
+
399
+ if (!can_cast_expr<dereference_exprt>(function))
400
+ return {};
401
+
402
+ auto const &function_pointer_call_site = to_symbol_expr (
403
+ to_dereference_expr (function)
404
+ .pointer ());
405
+
406
+ const goto_programt::const_targett it = std::prev (location);
407
+
408
+ const code_assignt &assign = it->get_assign ();
409
+
410
+ INVARIANT (
411
+ to_symbol_expr (assign.lhs ()).get_identifier () ==
412
+ function_pointer_call_site.get_identifier (),
413
+ " called function pointer must have been assigned at the previous location" );
414
+
415
+ if (!can_cast_expr<symbol_exprt>(assign.rhs ()))
416
+ return {};
417
+
418
+ const auto &rhs = to_symbol_expr (assign.rhs ());
419
+
420
+ const auto restriction = by_name_restrictions.find (rhs.get_identifier ());
421
+
422
+ if (restriction != by_name_restrictions.end ())
423
+ {
424
+ return optionalt<function_pointer_restrictionst::restrictiont>(
425
+ std::make_pair (
426
+ function_pointer_call_site.get_identifier (), restriction->second ));
427
+ }
428
+
429
+ return {};
430
+ }
431
+
434
432
function_pointer_restrictionst function_pointer_restrictionst::from_options (
435
433
const optionst &options,
436
434
const goto_modelt &goto_model,
@@ -562,8 +560,13 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
562
560
for_each_function_call (
563
561
goto_function.second ,
564
562
[&](const goto_programt::const_targett it) {
565
- get_by_name_restriction (
566
- goto_function.second , by_name_restrictions, restrictions, it);
563
+ const auto restriction = get_by_name_restriction (
564
+ goto_function.second , by_name_restrictions, it);
565
+
566
+ if (restriction)
567
+ {
568
+ restrictions.insert (*restriction);
569
+ }
567
570
});
568
571
}
569
572
0 commit comments