14 #include <unordered_set> 30 rename_symbol(
function.type);
34 rename_symbol(iit->code);
35 rename_symbol(iit->guard);
38 iit->function=new_function_name;
50 const std::unordered_set<irep_idt> &weak_symbols,
60 rename_symbolt::expr_mapt::const_iterator e_it=
61 rename_symbol.
expr_map.find(src_it->first);
65 if(e_it!=rename_symbol.
expr_map.end())
66 final_id=e_it->second;
69 goto_functionst::function_mapt::iterator dest_f_it=
76 dest_functions.
function_map.emplace(final_id, std::move(src_func));
82 if(in_dest_symbol_table.body.instructions.empty() ||
83 weak_symbols.find(final_id)!=weak_symbols.end())
88 in_dest_symbol_table.body.swap(src_func.body);
89 in_dest_symbol_table.type=src_func.type;
91 else if(src_func.body.instructions.empty() ||
92 src_ns.
lookup(src_it->first).is_weak)
96 else if(in_dest_symbol_table.type.get_bool(ID_C_inlined))
103 rename_symbol(src_func.type);
105 "linking ensures that types match");
113 for(
const auto &symbol_pair : dest_symbol_table.
symbols)
115 if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
117 const symbolt &symbol = symbol_pair.second;
125 std::cerr << symbol <<
'\n';
126 std::cerr << ns.
lookup(
id) <<
'\n';
136 if(!macro_application.
expr_map.empty())
143 if(!object_type_updates.
expr_map.empty())
148 object_type_updates(iit->code);
149 object_type_updates(iit->guard);
161 std::unordered_set<irep_idt> weak_symbols;
165 if(symbol_pair.second.is_weak)
166 weak_symbols.insert(symbol_pair.first);
irep_idt name
The unique identifier.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
const irep_idt & get_identifier() const
exprt value
Initial value of symbol.
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define INVARIANT(CONDITION, REASON)
const irep_idt & id() const
void link_goto_model(goto_modelt &dest, goto_modelt &src, message_handlert &message_handler)
::goto_functiont goto_functiont
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
static void rename_symbols_in_function(goto_functionst::goto_functiont &function, irep_idt &new_function_name, const rename_symbolt &rename_symbol)
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
goto_programt coverage_criteriont message_handlert & message_handler
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, const replace_symbolt &object_type_updates)
Link a set of goto functions, considering weak symbols and symbol renaming.
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().