35 (*this)(goto_model, replacement_map);
56 (*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;
100 if(next_it != goto_program.
instructions.end() && next_it->is_assign())
102 const exprt &rhs = next_it->assign_rhs();
106 "returns must not be removed before replacing calls");
121 for(
const std::string &s : replacement_list)
123 std::string original;
124 std::string replacement;
129 replacement_map.insert(std::make_pair(original, replacement));
134 "conflicting replacement for function " + original,
"--replace-calls");
138 return replacement_map;
146 for(
const auto &p : replacement_map)
148 if(replacement_map.find(p.second) != replacement_map.end())
151 " cannot both be replaced and be a replacement",
158 "replacement function " +
id2string(p.second) +
" needs to be present",
165 ns.
lookup(it1->first).type, ns.
lookup(it2->first).type, ns))
168 " are not type-compatible",
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
const typet & return_type() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool is_function_call() const
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
std::list< std::string > replacement_listt
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
std::map< irep_idt, irep_idt > replacement_mapt
void operator()(goto_modelt &goto_model, const replacement_listt &replacement_list) const
Replace function calls with calls to other functions.
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
Replace function returns by assignments to global variables.
Replace calls to given functions with calls to other given functions.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)