14#include <unordered_set>
28 for(
auto &identifier : function.parameter_identifiers)
30 auto entry = rename_symbol.
expr_map.find(identifier);
31 if(entry != rename_symbol.
expr_map.end())
32 identifier = entry->second;
35 for(
auto &instruction : function.body.instructions)
37 rename_symbol(instruction.code_nonconst());
39 if(instruction.has_condition())
41 exprt c = instruction.get_condition();
43 instruction.set_condition(
c);
65 rename_symbolt::expr_mapt::const_iterator
e_it =
74 goto_functionst::function_mapt::iterator
dest_f_it=
98 src_func.body.instructions.empty() ||
148 return linking.object_type_updates.get_expr_map();
177 std::cerr << symbol <<
'\n';
178 std::cerr << ns.lookup(
id) <<
'\n';
197 if(!object_type_updates.
empty())
201 for(
auto &instruction :
gf_entry.second.body.instructions)
203 instruction.transform([&object_type_updates](
exprt expr) {
204 object_type_updates(expr);
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
::goto_functiont goto_functiont
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
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().
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
const irep_idt & get_identifier() const
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
static void rename_symbols_in_function(goto_functionst::goto_functiont &function, irep_idt &new_function_name, const rename_symbolt &rename_symbol)
void finalize_linking(goto_modelt &dest, const replace_symbolt::expr_mapt &type_updates)
Apply type_updates to dest, where type_updates were constructed from one or more calls to link_goto_m...
optionalt< replace_symbolt::expr_mapt > link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &message_handler)
Link goto model src into goto model dest, invalidating src in this process.
static bool link_functions(symbol_tablet &dest_symbol_table, goto_functionst &dest_functions, const symbol_tablet &src_symbol_table, goto_functionst &src_functions, const rename_symbolt &rename_symbol, const std::unordered_set< irep_idt > &weak_symbols)
Link a set of goto functions, considering weak symbols and symbol renaming.
bool linking(symbol_tablet &dest_symbol_table, const symbol_tablet &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.