32 const std::string &filename,
52 return std::move(dest);
62 const std::string &filename,
85 message.
error() <<
"Failed to read header from '" << filename <<
"'"
92 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
95 in, filename, symbol_table, goto_functions, message_handler);
97 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
110 in, filename, symbol_table, goto_functions, message_handler);
115 "failed to find goto-cc section in ELF binary" <<
messaget::eom;
131 if(osx_fat_reader.
has_gb())
134 if(osx_fat_reader.
extract_gb(filename, tempname()))
145 temp_in, filename, symbol_table, goto_functions, message_handler);
152 message.
error() <<
"failed to find goto binary in Mach-O file"
164 osx_mach_o_readert::sectionst::const_iterator entry =
165 mach_o_reader.
sections.find(
"goto-cc");
166 if(entry != mach_o_reader.
sections.end())
168 in.seekg(entry->second.offset);
170 in, filename, symbol_table, goto_functions, message_handler);
175 <<
"failed to find goto-cc section in Mach-O binary" <<
messaget::eom;
193 const std::string &filename,
214 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
218 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
241 if(osx_fat_reader.
has_gb())
276 const std::string &file_name,
281 <<
"Reading GOTO program from file " << file_name <<
messaget::eom;
285 if(!temp_model.has_value())
292 const std::list<std::string> &file_names,
296 if(file_names.empty())
301 for(
const auto &file_name : file_names)
304 if(!updates_opt.has_value())
307 object_type_updates.insert(updates_opt->begin(), updates_opt->end());
void set_from_symbol_table(const symbol_tablet &)
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
std::string what() const override
A human readable description of what went wrong.
std::size_t number_of_sections
bool has_section(const std::string &name) const
std::string section_name(std::size_t index) const
std::streampos section_offset(std::size_t index) const
A collection of goto functions.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & status() const
bool extract_gb(const std::string &source, const std::string &dest) const
bool has_section(const std::string &name) const
std::unordered_map< irep_idt, exprt > expr_mapt
static std::string binary(const constant_exprt &src)
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.
nonstd::optional< T > optionalt
bool is_osx_fat_header(char header_bytes[8])
bool is_osx_mach_object(char hdr[4])
static bool read_bin_goto_object(std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
static optionalt< replace_symbolt::expr_mapt > read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file, and also updates config
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
bool read_objects_and_link(const std::list< std::string > &file_names, goto_modelt &dest, message_handlert &message_handler)
Reads object files and updates the config if any files were read.
std::wstring widen(const char *s)