@@ -238,15 +238,16 @@ function_pointer_restrictionst::merge_function_pointer_restrictions(
238238function_pointer_restrictionst::restrictionst
239239function_pointer_restrictionst::parse_function_pointer_restrictions (
240240 const std::list<std::string> &restriction_opts,
241- const std::string &option)
241+ const std::string &option,
242+ const goto_modelt &goto_model)
242243{
243244 auto function_pointer_restrictions =
244245 function_pointer_restrictionst::restrictionst{};
245246
246247 for (const std::string &restriction_opt : restriction_opts)
247248 {
248249 const auto restriction =
249- parse_function_pointer_restriction (restriction_opt, option);
250+ parse_function_pointer_restriction (restriction_opt, option, goto_model );
250251
251252 const bool inserted = function_pointer_restrictions
252253 .emplace (restriction.first , restriction.second )
@@ -265,10 +266,11 @@ function_pointer_restrictionst::parse_function_pointer_restrictions(
265266
266267function_pointer_restrictionst::restrictionst function_pointer_restrictionst::
267268 parse_function_pointer_restrictions_from_command_line (
268- const std::list<std::string> &restriction_opts)
269+ const std::list<std::string> &restriction_opts,
270+ const goto_modelt &goto_model)
269271{
270272 return parse_function_pointer_restrictions (
271- restriction_opts, " --" RESTRICT_FUNCTION_POINTER_OPT);
273+ restriction_opts, " --" RESTRICT_FUNCTION_POINTER_OPT, goto_model );
272274}
273275
274276function_pointer_restrictionst::restrictionst
@@ -292,7 +294,8 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
292294function_pointer_restrictionst::restrictiont
293295function_pointer_restrictionst::parse_function_pointer_restriction (
294296 const std::string &restriction_opt,
295- const std::string &option)
297+ const std::string &option,
298+ const goto_modelt &goto_model)
296299{
297300 // the format for restrictions is <pointer_name>/<target[,more_targets]*>
298301 // exactly one pointer and at least one target
@@ -321,7 +324,52 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
321324 " couldn't find target name before '/' in `" + restriction_opt + " '" };
322325 }
323326
324- auto const pointer_name = restriction_opt.substr (0 , pointer_name_end);
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+ }
372+
325373 auto const target_names_substring =
326374 restriction_opt.substr (pointer_name_end + 1 );
327375 auto const target_name_strings = split_string (target_names_substring, ' ,' );
@@ -405,7 +453,8 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
405453 try
406454 {
407455 commandline_restrictions =
408- parse_function_pointer_restrictions_from_command_line (restriction_opts);
456+ parse_function_pointer_restrictions_from_command_line (
457+ restriction_opts, goto_model);
409458 typecheck_function_pointer_restrictions (
410459 goto_model, commandline_restrictions);
411460 }
@@ -549,7 +598,9 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
549598{
550599 function_pointer_restrictionst::restrictionst by_name_restrictions =
551600 parse_function_pointer_restrictions (
552- restriction_name_opts, " --" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
601+ restriction_name_opts,
602+ " --" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT,
603+ goto_model);
553604
554605 function_pointer_restrictionst::restrictionst restrictions;
555606 for (auto const &goto_function : goto_model.goto_functions .function_map )
0 commit comments