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;
103 if(next_it != goto_program.
instructions.end() && next_it->is_assign())
110 "returns must not be removed before replacing calls");
115 function.type() = f_it2->second.type;
127 for(
const std::string &s : replacement_list)
129 std::string original;
130 std::string replacement;
135 replacement_map.insert(std::make_pair(original, replacement));
140 "conflicting replacement for function " + original,
"--replace-calls");
144 return replacement_map;
152 for(
const auto &p : replacement_map)
154 if(replacement_map.find(p.second) != replacement_map.end())
157 " cannot both be replaced and be a replacement",
164 "replacement function " +
id2string(p.second) +
" needs to be present",
170 if(!
base_type_eq(it1->second.type, it2->second.type, ns))
173 " 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...
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.
const irep_idt & id() const
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
const typet & return_type() const
instructionst::const_iterator const_targett
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)