@@ -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,52 @@ 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
+ // 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
+
434
435
function_pointer_restrictionst function_pointer_restrictionst::from_options (
435
436
const optionst &options,
436
437
const goto_modelt &goto_model,
@@ -562,8 +563,13 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions(
562
563
for_each_function_call (
563
564
goto_function.second ,
564
565
[&](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
+ }
567
573
});
568
574
}
569
575
0 commit comments