cprover
|
#include <replace_calls.h>
Public Types | |
typedef std::list< std::string > | replacement_listt |
typedef std::map< irep_idt, irep_idt > | replacement_mapt |
Public Member Functions | |
void | operator() (goto_modelt &goto_model, const replacement_listt &replacement_list) const |
Replace function calls with calls to other functions. More... | |
void | operator() (goto_modelt &goto_model, const replacement_mapt &replacement_map) const |
Replace function calls with calls to other functions. More... | |
Protected Member Functions | |
void | operator() (goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns, const replacement_mapt &replacement_map) const |
replacement_mapt | parse_replacement_list (const replacement_listt &replacement_list) const |
void | check_replacement_map (const replacement_mapt &replacement_map, const goto_functionst &goto_functions, const namespacet &ns) const |
Definition at line 18 of file replace_calls.h.
typedef std::list<std::string> replace_callst::replacement_listt |
Definition at line 21 of file replace_calls.h.
typedef std::map<irep_idt, irep_idt> replace_callst::replacement_mapt |
Definition at line 22 of file replace_calls.h.
|
protected |
Definition at line 141 of file replace_calls.cpp.
References base_type_eq(), goto_functionst::function_map, and id2string().
Referenced by operator()().
void replace_callst::operator() | ( | goto_modelt & | goto_model, |
const replacement_listt & | replacement_list | ||
) | const |
Replace function calls with calls to other functions.
goto_model | goto model to modify |
replacement_list | list of strings, with each string f:g denoting a mapping between functions names; a mapping f -> g indicates that calls to f should be replaced by calls to g |
Definition at line 29 of file replace_calls.cpp.
References parse_replacement_list().
void replace_callst::operator() | ( | goto_modelt & | goto_model, |
const replacement_mapt & | replacement_map | ||
) | const |
Replace function calls with calls to other functions.
goto_model | goto model to modify |
replacement_map | mapping between function names; a mapping f -> g indicates that calls to f should be replaced by calls to g |
Definition at line 41 of file replace_calls.cpp.
References check_replacement_map(), goto_functionst::function_map, goto_modelt::goto_functions, goto_program, and goto_modelt::symbol_table.
|
protected |
Definition at line 59 of file replace_calls.cpp.
References base_type_eq(), goto_programt::instructiont::code, DATA_INVARIANT, Forall_goto_program_instructions, code_function_callt::function(), goto_functionst::function_map, symbol_exprt::get_identifier(), goto_program, has_suffix(), irept::id(), id2string(), goto_programt::instructions, goto_programt::instructiont::is_function_call(), PRECONDITION, RETURN_VALUE_SUFFIX, code_assignt::rhs(), symbol_exprt::set_identifier(), to_code_assign(), to_code_function_call(), and to_symbol_expr().
|
protected |
Definition at line 119 of file replace_calls.cpp.
References r, and split_string().
Referenced by operator()().