14 #if defined(__linux__) || \ 15 defined(__FreeBSD_kernel__) || \ 17 defined(__unix__) || \ 18 defined(__CYGWIN__) || \ 24 #include <unordered_set> 42 const std::string &filename,
51 const std::string &filename,
57 std::ifstream in(
widen(filename), std::ios::binary);
59 std::ifstream in(filename, std::ios::binary);
65 message.
error() <<
"Failed to open `" << filename <<
"'" 77 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
80 in, filename, symbol_table, goto_functions, message_handler);
82 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
95 in, filename, symbol_table, goto_functions, message_handler);
100 "failed to find goto-cc section in ELF binary" <<
messaget::eom;
110 std::string tempname;
117 if(osx_fat_reader.
has_gb())
120 osx_fat_reader.
extract_gb(filename, tempname);
122 std::ifstream temp_in(tempname, std::ios::binary);
124 messaget(message_handler).
error() <<
"failed to read temp binary" 127 temp_in, filename, symbol_table, goto_functions, message_handler);
130 unlink(tempname.c_str());
136 "failed to find goto binary in Mach-O file" <<
messaget::eom;
141 if(!tempname.empty())
142 unlink(tempname.c_str());
158 std::ifstream in(
widen(filename), std::ios::binary);
160 std::ifstream in(filename, std::ios::binary);
176 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
180 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
203 if(osx_fat_reader.
has_gb())
221 rename_symbol(
function.type);
225 rename_symbol(iit->code);
226 rename_symbol(iit->guard);
236 const std::unordered_set<irep_idt, irep_id_hash> &weak_symbols,
246 rename_symbolt::expr_mapt::const_iterator e_it=
247 rename_symbol.
expr_map.find(src_it->first);
251 if(e_it!=rename_symbol.
expr_map.end())
252 final_id=e_it->second;
255 goto_functionst::function_mapt::iterator dest_f_it=
265 in_dest_symbol_table.body.swap(src_it->second.body);
266 in_dest_symbol_table.type=src_it->second.type;
275 if(in_dest_symbol_table.body.instructions.empty() ||
276 weak_symbols.find(final_id)!=weak_symbols.end())
281 in_dest_symbol_table.body.swap(src_func.body);
282 in_dest_symbol_table.type=src_func.type;
284 else if(src_func.body.instructions.empty() ||
285 src_ns.
lookup(src_it->first).is_weak)
289 else if(in_dest_symbol_table.type.get_bool(ID_C_inlined))
296 rename_symbol(src_func.type);
297 assert(
base_type_eq(in_dest_symbol_table.type, src_func.type, ns));
306 if(it->second.is_macro && !it->second.is_type)
308 const symbolt &symbol=it->second;
310 assert(symbol.
value.
id()==ID_symbol);
316 std::cerr << symbol <<
'\n';
317 std::cerr << ns.
lookup(
id) <<
'\n';
325 if(!macro_application.
expr_map.empty())
329 if(!object_type_updates.
expr_map.empty())
334 object_type_updates(iit->code);
335 object_type_updates(iit->guard);
346 const std::string &file_name,
363 typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
364 id_sett weak_symbols;
366 if(it->second.is_weak)
367 weak_symbols.insert(it->first);
393 const std::string &file_name,
bool has_section(const std::string &name) const
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
#define forall_symbols(it, expr)
std::wstring widen(const char *s)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
const irep_idt & get_identifier() const
bool is_goto_binary(const std::string &filename)
std::string section_name(unsigned index) const
exprt value
Initial value of symbol.
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
symbol_tablet symbol_table
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
static void rename_symbols_in_function(goto_functionst::goto_functiont &function, const rename_symbolt &rename_symbol)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
const irep_idt & id() const
bool extract_gb(const std::string &source, const std::string &dest) const
unsigned number_of_sections
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, irep_id_hash > &weak_symbols, const replace_symbolt &object_type_updates)
goto_function_templatet< goto_programt > goto_functiont
function_mapt function_map
bool read_object_and_link(const std::string &file_name, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads an object file
bool read_bin_goto_object(std::istream &in, const std::string &filename, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads a goto binary file back into a symbol and a function table
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool is_osx_fat_magic(char hdr[4])
typet type
Type of symbol.
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
std::streampos section_offset(unsigned index) const
goto_functionst goto_functions