cprover
|
Public Types | |
using | functionst = remove_const_function_pointerst::functionst |
Public Member Functions | |
remove_function_pointerst (message_handlert &_message_handler, symbol_tablet &_symbol_table, bool _add_safety_assertion, bool only_resolve_const_fps, const goto_functionst &goto_functions) | |
void | operator() (goto_functionst &goto_functions) |
bool | remove_function_pointers (goto_programt &goto_program, const irep_idt &function_id) |
void | remove_function_pointer (goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, const functionst &functions) |
Replace a call to a dynamic function at location target in the given goto-program by a case-split over a given set of functions. More... | |
Protected Types | |
typedef std::map< irep_idt, code_typet > | type_mapt |
Protected Member Functions | |
void | remove_function_pointer (goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target) |
Replace a call to a dynamic function at location target in the given goto-program by determining functions that have a compatible signature. More... | |
bool | is_type_compatible (bool return_value_used, const code_typet &call_type, const code_typet &function_type) |
bool | arg_is_type_compatible (const typet &call_type, const typet &function_type) |
void | fix_argument_types (code_function_callt &function_call) |
void | fix_return_type (const irep_idt &in_function_id, code_function_callt &function_call, goto_programt &dest) |
Protected Attributes | |
messaget | log |
const namespacet | ns |
symbol_tablet & | symbol_table |
bool | add_safety_assertion |
bool | only_resolve_const_fps |
std::unordered_set< irep_idt > | address_taken |
type_mapt | type_map |
Definition at line 31 of file remove_function_pointers.cpp.
Definition at line 48 of file remove_function_pointers.cpp.
|
protected |
Definition at line 90 of file remove_function_pointers.cpp.
remove_function_pointerst::remove_function_pointerst | ( | message_handlert & | _message_handler, |
symbol_tablet & | _symbol_table, | ||
bool | _add_safety_assertion, | ||
bool | only_resolve_const_fps, | ||
const goto_functionst & | goto_functions | ||
) |
Definition at line 109 of file remove_function_pointers.cpp.
|
protected |
Definition at line 131 of file remove_function_pointers.cpp.
|
protected |
Definition at line 207 of file remove_function_pointers.cpp.
|
protected |
Definition at line 231 of file remove_function_pointers.cpp.
|
protected |
Definition at line 157 of file remove_function_pointers.cpp.
void remove_function_pointerst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 500 of file remove_function_pointers.cpp.
|
protected |
Replace a call to a dynamic function at location target in the given goto-program by determining functions that have a compatible signature.
goto_program | The goto program that contains target |
function_id | Name of function containing the target |
target | location with function call with function pointer |
Definition at line 266 of file remove_function_pointers.cpp.
void remove_function_pointerst::remove_function_pointer | ( | goto_programt & | goto_program, |
const irep_idt & | function_id, | ||
goto_programt::targett | target, | ||
const functionst & | functions | ||
) |
Replace a call to a dynamic function at location target in the given goto-program by a case-split over a given set of functions.
goto_program | The goto program that contains target |
function_id | Name of function containing the target |
target | location with function call with function pointer |
functions | The set of functions to consider |
Definition at line 362 of file remove_function_pointers.cpp.
bool remove_function_pointerst::remove_function_pointers | ( | goto_programt & | goto_program, |
const irep_idt & | function_id | ||
) |
Definition at line 476 of file remove_function_pointers.cpp.
|
protected |
Definition at line 67 of file remove_function_pointers.cpp.
|
protected |
Definition at line 88 of file remove_function_pointers.cpp.
|
protected |
Definition at line 64 of file remove_function_pointers.cpp.
|
protected |
Definition at line 65 of file remove_function_pointers.cpp.
|
protected |
Definition at line 75 of file remove_function_pointers.cpp.
|
protected |
Definition at line 66 of file remove_function_pointers.cpp.
|
protected |
Definition at line 91 of file remove_function_pointers.cpp.