14 #include <unordered_set> 31 rename_symbol(
function.type);
35 rename_symbol(iit->code);
36 rename_symbol(iit->guard);
39 iit->function=new_function_name;
51 const std::unordered_set<irep_idt> &weak_symbols,
61 rename_symbolt::expr_mapt::const_iterator e_it=
62 rename_symbol.
expr_map.find(src_it->first);
66 if(e_it!=rename_symbol.
expr_map.end())
67 final_id=e_it->second;
70 goto_functionst::function_mapt::iterator dest_f_it=
77 dest_functions.
function_map.emplace(final_id, std::move(src_func));
83 if(in_dest_symbol_table.body.instructions.empty() ||
84 weak_symbols.find(final_id)!=weak_symbols.end())
89 in_dest_symbol_table.body.swap(src_func.body);
90 in_dest_symbol_table.type=src_func.type;
92 else if(src_func.body.instructions.empty() ||
93 src_ns.
lookup(src_it->first).is_weak)
97 else if(in_dest_symbol_table.type.get_bool(ID_C_inlined))
104 rename_symbol(src_func.type);
106 "linking ensures that types match");
114 for(
const auto &symbol_pair : dest_symbol_table.
symbols)
116 if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
118 const symbolt &symbol = symbol_pair.second;
126 std::cerr << symbol <<
'\n';
127 std::cerr << ns.
lookup(
id) <<
'\n';
137 if(!macro_application.
expr_map.empty())
144 if(!object_type_updates.
empty())
149 object_type_updates(iit->code);
150 object_type_updates(iit->guard);
162 std::unordered_set<irep_idt> weak_symbols;
166 if(symbol_pair.second.is_weak)
167 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)
Check types for equality across all levels of hierarchy.
const irep_idt & get_identifier() const
exprt value
Initial value of symbol.
Thrown when we can't handle something in an input source file.
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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const irep_idt & id() const
void link_goto_model(goto_modelt &dest, goto_modelt &src, message_handlert &message_handler)
Replace expression or type symbols by an expression or type, respectively.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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)
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 documentation for namespace_baset::lookup().