@@ -84,14 +84,14 @@ static void restrict_function_pointer(
8484}
8585} // namespace
8686
87- function_pointer_restrictionst::invalid_restriction_exceptiont::
88- invalid_restriction_exceptiont (std::string reason, std::string correct_format)
87+ invalid_restriction_exceptiont::invalid_restriction_exceptiont (
88+ std::string reason,
89+ std::string correct_format)
8990 : reason(std::move(reason)), correct_format(std::move(correct_format))
9091{
9192}
9293
93- std::string
94- function_pointer_restrictionst::invalid_restriction_exceptiont::what () const
94+ std::string invalid_restriction_exceptiont::what () const
9595{
9696 std::string res;
9797
@@ -291,6 +291,66 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
291291 return merged_restrictions;
292292}
293293
294+ // / Parse \p candidate to distinguish whether it refers to a function pointer
295+ // / symbol directly (as produced by \ref label_function_pointer_call_sites), or
296+ // / a source location via its statement label. In the latter case, resolve the
297+ // / name to the underlying function pointer symbol.
298+ static std::string resolve_pointer_name (
299+ const std::string &candidate,
300+ const goto_modelt &goto_model)
301+ {
302+ const auto last_dot = candidate.rfind (' .' );
303+ if (
304+ last_dot == std::string::npos || last_dot + 1 == candidate.size () ||
305+ isdigit (candidate[last_dot + 1 ]))
306+ {
307+ return candidate;
308+ }
309+
310+ std::string pointer_name = candidate;
311+
312+ const auto function_id = pointer_name.substr (0 , last_dot);
313+ const auto label = pointer_name.substr (last_dot + 1 );
314+
315+ bool found = false ;
316+ const auto it = goto_model.goto_functions .function_map .find (function_id);
317+ if (it != goto_model.goto_functions .function_map .end ())
318+ {
319+ optionalt<source_locationt> location;
320+ for (const auto &instruction : it->second .body .instructions )
321+ {
322+ if (
323+ std::find (
324+ instruction.labels .begin (), instruction.labels .end (), label) !=
325+ instruction.labels .end ())
326+ {
327+ location = instruction.source_location ();
328+ }
329+
330+ if (
331+ instruction.is_function_call () &&
332+ instruction.call_function ().id () == ID_dereference &&
333+ location.has_value () && instruction.source_location () == *location)
334+ {
335+ auto const &called_function_pointer =
336+ to_dereference_expr (instruction.call_function ()).pointer ();
337+ pointer_name =
338+ id2string (to_symbol_expr (called_function_pointer).get_identifier ());
339+ found = true ;
340+ break ;
341+ }
342+ }
343+ }
344+ if (!found)
345+ {
346+ throw invalid_restriction_exceptiont{
347+ " non-existent pointer name " + pointer_name,
348+ " pointers should be identifiers or <function_name>.<label>" };
349+ }
350+
351+ return pointer_name;
352+ }
353+
294354function_pointer_restrictionst::restrictiont
295355function_pointer_restrictionst::parse_function_pointer_restriction (
296356 const std::string &restriction_opt,
@@ -324,51 +384,8 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
324384 " couldn't find target name before '/' in `" + restriction_opt + " '" };
325385 }
326386
327- auto pointer_name = restriction_opt.substr (0 , pointer_name_end);
328- const auto last_dot = pointer_name.rfind (' .' );
329- if (
330- last_dot != std::string::npos && last_dot + 1 != pointer_name.size () &&
331- !isdigit (pointer_name[last_dot + 1 ]))
332- {
333- const auto function_id = pointer_name.substr (0 , last_dot);
334- const auto label = pointer_name.substr (last_dot + 1 );
335-
336- bool found = false ;
337- const auto it = goto_model.goto_functions .function_map .find (function_id);
338- if (it != goto_model.goto_functions .function_map .end ())
339- {
340- optionalt<source_locationt> location;
341- for (const auto &instruction : it->second .body .instructions )
342- {
343- if (
344- std::find (
345- instruction.labels .begin (), instruction.labels .end (), label) !=
346- instruction.labels .end ())
347- {
348- location = instruction.source_location ();
349- }
350-
351- if (
352- instruction.is_function_call () &&
353- instruction.call_function ().id () == ID_dereference &&
354- location.has_value () && instruction.source_location () == *location)
355- {
356- auto const &called_function_pointer =
357- to_dereference_expr (instruction.call_function ()).pointer ();
358- pointer_name =
359- id2string (to_symbol_expr (called_function_pointer).get_identifier ());
360- found = true ;
361- break ;
362- }
363- }
364- }
365- if (!found)
366- {
367- throw invalid_restriction_exceptiont{" non-existent pointer name " +
368- pointer_name,
369- restriction_format_message};
370- }
371- }
387+ std::string pointer_name = resolve_pointer_name (
388+ restriction_opt.substr (0 , pointer_name_end), goto_model);
372389
373390 auto const target_names_substring =
374391 restriction_opt.substr (pointer_name_end + 1 );
0 commit comments