34 (*this)(goto_model, replacement_map);
55 (*this)(
goto_program, goto_functions, ns, replacement_map);
84 "Called functions need to be present");
86 replacement_mapt::const_iterator r_it = replacement_map.find(
id);
88 if(r_it == replacement_map.end())
91 const irep_idt &new_id = r_it->second;
105 if(rhs.
id() == ID_symbol)
109 throw "Returns must not be removed before replacing calls";
114 function.type() = f_it2->second.type;
124 for(
const std::string &s : replacement_list)
126 std::string original;
127 std::string replacement;
132 replacement_map.insert(std::make_pair(original, replacement));
135 throw "Conflicting replacement for function " + original;
138 return replacement_map;
146 for(
const auto &p : replacement_map)
148 if(replacement_map.find(p.second) != replacement_map.end())
149 throw "Function " +
id2string(p.second) +
150 " cannot both be replaced and " 156 throw "Replacement function " +
id2string(p.second) +
157 " needs to be present";
162 if(!
base_type_eq(it1->second.type, it2->second.type, ns))
163 throw "Functions " +
id2string(p.first) +
" and " +
164 id2string(p.second) +
" are not type-compatible";
void check_replacement_map(const replacement_mapt &replacement_map, const goto_functionst &goto_functions, const namespacet &ns) const
replacement_mapt parse_replacement_list(const replacement_listt &replacement_list) const
const std::string & id2string(const irep_idt &d)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool is_function_call() const
const irep_idt & get_identifier() const
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
void operator()(goto_modelt &goto_model, const replacement_listt &replacement_list) const
Replace function calls with calls to other functions.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A generic container class for the GOTO intermediate representation of one function.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter...
Replace calls to given functions with calls to other given functions.
Base class for all expressions.
void set_identifier(const irep_idt &identifier)
goto_programt & goto_program
std::list< std::string > replacement_listt
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
bool has_suffix(const std::string &s, const std::string &suffix)
#define RETURN_VALUE_SUFFIX
#define DATA_INVARIANT(CONDITION, REASON)
goto_functionst goto_functions
GOTO functions.
std::map< irep_idt, irep_idt > replacement_mapt
const code_function_callt & to_code_function_call(const codet &code)