cprover
|
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) |
Protected Types | |
typedef std::map< irep_idt, code_typet > | type_mapt |
Protected Member Functions | |
void | remove_function_pointer (goto_programt &goto_program, goto_programt::targett target) |
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 (code_function_callt &function_call, goto_programt &dest) |
void | compute_address_taken_in_symbols (std::set< irep_idt > &address_taken) |
Protected Attributes | |
const namespacet | ns |
symbol_tablet & | symbol_table |
bool | add_safety_assertion |
bool | only_resolve_const_fps |
std::set< irep_idt > | address_taken |
type_mapt | type_map |
Additional Inherited Members |
Definition at line 33 of file remove_function_pointers.cpp.
|
protected |
Definition at line 66 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 93 of file remove_function_pointers.cpp.
References address_taken, compute_address_taken_functions(), compute_address_taken_in_symbols(), forall_goto_functions, and type_map.
|
protected |
Definition at line 112 of file remove_function_pointers.cpp.
References irept::id(), ns, and type_eq().
Referenced by is_type_compatible().
|
inlineprotected |
Definition at line 83 of file remove_function_pointers.cpp.
References compute_address_taken_functions(), namespacet::get_symbol_table(), and symbol_tablet::symbols.
Referenced by remove_function_pointerst().
|
protected |
Definition at line 194 of file remove_function_pointers.cpp.
References code_function_callt::arguments(), namespace_baset::follow(), code_function_callt::function(), ns, code_typet::parameters(), to_code_type(), exprt::type(), and type_eq().
Referenced by remove_function_pointer().
|
protected |
Definition at line 219 of file remove_function_pointers.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), namespace_baset::follow(), code_function_callt::function(), get_fresh_aux_symbol(), irept::is_nil(), code_function_callt::lhs(), symbolt::name, ns, code_typet::return_type(), exprt::source_location(), symbol_table, to_code_type(), symbolt::type, exprt::type(), and type_eq().
Referenced by remove_function_pointer().
|
protected |
Definition at line 144 of file remove_function_pointers.cpp.
References arg_is_type_compatible(), code_typet::has_ellipsis(), ns, code_typet::parameters(), code_typet::return_type(), and type_eq().
Referenced by remove_function_pointer().
void remove_function_pointerst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 462 of file remove_function_pointers.cpp.
References goto_functions_templatet< bodyT >::compute_location_numbers(), goto_functions_templatet< bodyT >::function_map, and remove_function_pointers().
|
protected |
Definition at line 258 of file remove_function_pointers.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), add_safety_assertion, exprt::add_source_location(), address_taken, code_function_callt::arguments(), CHECK_RETURN, comment(), goto_program_templatet< codeT, guardT >::destructive_append(), goto_program_templatet< codeT, guardT >::destructive_insert(), dstringt::empty(), messaget::eom(), code_expressiont::expression(), fix_argument_types(), fix_return_type(), forall_expr, Forall_goto_program_instructions, code_function_callt::function(), messaget::get_message_handler(), code_typet::has_ellipsis(), irept::is_not_nil(), is_type_compatible(), code_function_callt::lhs(), exprt::make_typecast(), ns, only_resolve_const_fps, exprt::op0(), OTHER, code_typet::parameters(), pointer_type(), code_typet::remove_ellipsis(), symbol_exprt::set_identifier(), messaget::mstreamt::source_location, messaget::statistics(), irept::swap(), symbol_table, to_code_function_call(), to_code_type(), exprt::type(), type_map, and messaget::warning().
Referenced by remove_function_pointers().
bool remove_function_pointerst::remove_function_pointers | ( | goto_programt & | goto_program | ) |
Definition at line 435 of file remove_function_pointers.cpp.
References Forall_goto_program_instructions, code_function_callt::function(), irept::id(), remove_function_pointer(), remove_skip(), to_code_function_call(), and goto_program_templatet< codeT, guardT >::update().
Referenced by operator()(), and remove_function_pointers().
|
protected |
Definition at line 50 of file remove_function_pointers.cpp.
Referenced by remove_function_pointer().
|
protected |
Definition at line 64 of file remove_function_pointers.cpp.
Referenced by remove_function_pointer(), and remove_function_pointerst().
|
protected |
Definition at line 48 of file remove_function_pointers.cpp.
Referenced by arg_is_type_compatible(), fix_argument_types(), fix_return_type(), is_type_compatible(), and remove_function_pointer().
|
protected |
Definition at line 58 of file remove_function_pointers.cpp.
Referenced by remove_function_pointer().
|
protected |
Definition at line 49 of file remove_function_pointers.cpp.
Referenced by fix_return_type(), and remove_function_pointer().
|
protected |
Definition at line 67 of file remove_function_pointers.cpp.
Referenced by remove_function_pointer(), and remove_function_pointerst().