Go to the documentation of this file.
35 (*this)(goto_model, replacement_map);
56 (*this)(goto_program, goto_functions, ns, replacement_map);
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;
101 if(next_it != goto_program.
instructions.end() && next_it->is_assign())
106 if(rhs.
id() == ID_symbol)
111 "returns must not be removed before replacing calls");
116 function.type() = f_it2->second.type;
126 for(
const std::string &s : replacement_list)
128 std::string original;
129 std::string replacement;
134 replacement_map.insert(std::make_pair(original, replacement));
139 "conflicting replacement for function " + original,
"--replace-calls");
143 return replacement_map;
151 for(
const auto &p : replacement_map)
153 if(replacement_map.find(p.second) != replacement_map.end())
156 " cannot both be replaced and be a replacement",
163 "replacement function " +
id2string(p.second) +
" needs to be present",
169 if(!
base_type_eq(it1->second.type, it2->second.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.
#define PRECONDITION(CONDITION)
std::list< std::string > replacement_listt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Base class for all expressions.
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
bool has_suffix(const std::string &s, const std::string &suffix)
replacement_mapt parse_replacement_list(const replacement_listt &replacement_list) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
codet representation of a function call statement.
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.
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.
const irep_idt & get_identifier() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
#define RETURN_VALUE_SUFFIX
::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.
const code_assignt & to_code_assign(const codet &code)
A generic container class for the GOTO intermediate representation of one function.
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)