@@ -198,51 +198,6 @@ void restrict_function_pointer(
198198 address_of_exprt{function_pointer_target_symbol_expr}}));
199199 }
200200}
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- }
246201} // namespace
247202
248203void restrict_function_pointers (
@@ -431,6 +386,52 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
431386 return std::make_pair (pointer_name, target_names);
432387}
433388
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+ // the function pointer is guaranteed to be a symbol expression, as the
403+ // label_function_pointer_call_sites() pass (which must be run before the
404+ // function pointer restriction) replaces calls via complex pointer
405+ // expressions by calls to a function pointer variable
406+ auto const &function_pointer_call_site =
407+ to_symbol_expr (to_dereference_expr (function).pointer ());
408+
409+ const goto_programt::const_targett it = std::prev (location);
410+
411+ const code_assignt &assign = it->get_assign ();
412+
413+ INVARIANT (
414+ to_symbol_expr (assign.lhs ()).get_identifier () ==
415+ function_pointer_call_site.get_identifier (),
416+ " called function pointer must have been assigned at the previous location" );
417+
418+ if (!can_cast_expr<symbol_exprt>(assign.rhs ()))
419+ return {};
420+
421+ const auto &rhs = to_symbol_expr (assign.rhs ());
422+
423+ const auto restriction = by_name_restrictions.find (rhs.get_identifier ());
424+
425+ if (restriction != by_name_restrictions.end ())
426+ {
427+ return optionalt<function_pointer_restrictionst::restrictiont>(
428+ std::make_pair (
429+ function_pointer_call_site.get_identifier (), restriction->second ));
430+ }
431+
432+ return {};
433+ }
434+
434435function_pointer_restrictionst function_pointer_restrictionst::from_options (
435436 const optionst &options,
436437 const goto_modelt &goto_model,
@@ -562,8 +563,13 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
562563 for_each_function_call (
563564 goto_function.second ,
564565 [&](const goto_programt::const_targett it) {
565- get_by_name_restriction (
566- goto_function.second , by_name_restrictions, restrictions, it);
566+ const auto restriction = get_by_name_restriction (
567+ goto_function.second , by_name_restrictions, it);
568+
569+ if (restriction)
570+ {
571+ restrictions.insert (*restriction);
572+ }
567573 });
568574 }
569575
0 commit comments