@@ -238,15 +238,16 @@ function_pointer_restrictionst::merge_function_pointer_restrictions(
238
238
function_pointer_restrictionst::restrictionst
239
239
function_pointer_restrictionst::parse_function_pointer_restrictions (
240
240
const std::list<std::string> &restriction_opts,
241
- const std::string &option)
241
+ const std::string &option,
242
+ const goto_modelt &goto_model)
242
243
{
243
244
auto function_pointer_restrictions =
244
245
function_pointer_restrictionst::restrictionst{};
245
246
246
247
for (const std::string &restriction_opt : restriction_opts)
247
248
{
248
249
const auto restriction =
249
- parse_function_pointer_restriction (restriction_opt, option);
250
+ parse_function_pointer_restriction (restriction_opt, option, goto_model );
250
251
251
252
const bool inserted = function_pointer_restrictions
252
253
.emplace (restriction.first , restriction.second )
@@ -265,10 +266,11 @@ function_pointer_restrictionst::parse_function_pointer_restrictions(
265
266
266
267
function_pointer_restrictionst::restrictionst function_pointer_restrictionst::
267
268
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)
269
271
{
270
272
return parse_function_pointer_restrictions (
271
- restriction_opts, " --" RESTRICT_FUNCTION_POINTER_OPT);
273
+ restriction_opts, " --" RESTRICT_FUNCTION_POINTER_OPT, goto_model );
272
274
}
273
275
274
276
function_pointer_restrictionst::restrictionst
@@ -292,7 +294,8 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file(
292
294
function_pointer_restrictionst::restrictiont
293
295
function_pointer_restrictionst::parse_function_pointer_restriction (
294
296
const std::string &restriction_opt,
295
- const std::string &option)
297
+ const std::string &option,
298
+ const goto_modelt &goto_model)
296
299
{
297
300
// the format for restrictions is <pointer_name>/<target[,more_targets]*>
298
301
// exactly one pointer and at least one target
@@ -321,7 +324,52 @@ function_pointer_restrictionst::parse_function_pointer_restriction(
321
324
" couldn't find target name before '/' in `" + restriction_opt + " '" };
322
325
}
323
326
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
+
325
373
auto const target_names_substring =
326
374
restriction_opt.substr (pointer_name_end + 1 );
327
375
auto const target_name_strings = split_string (target_names_substring, ' ,' );
@@ -405,7 +453,8 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options(
405
453
try
406
454
{
407
455
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);
409
458
typecheck_function_pointer_restrictions (
410
459
goto_model, commandline_restrictions);
411
460
}
@@ -549,7 +598,9 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
549
598
{
550
599
function_pointer_restrictionst::restrictionst by_name_restrictions =
551
600
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);
553
604
554
605
function_pointer_restrictionst::restrictionst restrictions;
555
606
for (auto const &goto_function : goto_model.goto_functions .function_map )
0 commit comments