Go to the documentation of this file.
35 (*this)(goto_model, replacement_map);
56 (*this)(goto_program, goto_functions, ns, replacement_map);
74 exprt &
function = cfc.function();
85 "Called functions need to be present");
87 replacement_mapt::const_iterator r_it = replacement_map.find(
id);
89 if(r_it == replacement_map.end())
92 const irep_idt &new_id = r_it->second;
98 if(
to_code_type(
function.type()).return_type().
id() != ID_empty)
101 if(next_it != goto_program.
instructions.end() && next_it->is_assign())
108 "returns must not be removed before replacing calls");
113 function.type() = ns.
lookup(f_it2->first).type;
125 for(
const std::string &s : replacement_list)
127 std::string original;
128 std::string replacement;
133 replacement_map.insert(std::make_pair(original, replacement));
138 "conflicting replacement for function " + original,
"--replace-calls");
142 return replacement_map;
150 for(
const auto &p : replacement_map)
152 if(replacement_map.find(p.second) != replacement_map.end())
155 " cannot both be replaced and be a replacement",
162 "replacement function " +
id2string(p.second) +
" needs to be present",
169 ns.
lookup(it1->first).type, ns.
lookup(it2->first).type, ns))
172 " are not type-compatible",
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::list< std::string > replacement_listt
Base class for all expressions.
Replace calls to given functions with calls to other given functions.
function_mapt function_map
Expression to hold a symbol (variable)
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
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
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().
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
std::map< irep_idt, irep_idt > replacement_mapt
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Replace function returns by assignments to global variables.
::goto_functiont goto_functiont
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
void operator()(goto_modelt &goto_model, const replacement_listt &replacement_list) const
Replace function calls with calls to other functions.
A generic container class for the GOTO intermediate representation of one function.
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
instructionst::const_iterator const_targett
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A codet representing an assignment in the program.
bool is_function_call() const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
void set_identifier(const irep_idt &identifier)