29 const std::string &filename,
38 std::optional<goto_modelt>
49 return std::move(dest);
59 const std::string &filename,
78 message.
error() <<
"Failed to read header from '" << filename <<
"'"
85 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
88 in, filename, symbol_table, goto_functions, message_handler);
90 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
103 in, filename, symbol_table, goto_functions, message_handler);
108 "failed to find goto-cc section in ELF binary" <<
messaget::eom;
124 if(osx_fat_reader.
has_gb())
127 if(osx_fat_reader.
extract_gb(filename, tempname()))
138 temp_in, filename, symbol_table, goto_functions, message_handler);
145 message.
error() <<
"failed to find goto binary in Mach-O file"
157 osx_mach_o_readert::sectionst::const_iterator entry =
158 mach_o_reader.
sections.find(
"goto-cc");
159 if(entry != mach_o_reader.
sections.end())
161 in.seekg(entry->second.offset);
163 in, filename, symbol_table, goto_functions, message_handler);
168 <<
"failed to find goto-cc section in Mach-O binary" <<
messaget::eom;
186 const std::string &filename,
203 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
207 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
230 if(osx_fat_reader.
has_gb())
265 const std::string &file_name,
270 <<
"Reading GOTO program from file " << file_name <<
messaget::eom;
274 if(!temp_model.has_value())
281 const std::list<std::string> &file_names,
285 if(file_names.empty())
290 for(
const auto &file_name : file_names)
293 if(!updates_opt.has_value())
296 object_type_updates.insert(updates_opt->begin(), updates_opt->end());
void set_from_symbol_table(const symbol_table_baset &)
virtual std::string what() const
A human readable description of what went wrong.
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
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)
std::optional< 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.
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...
bool is_osx_fat_header(char header_bytes[8])
bool is_osx_mach_object(char hdr[4])
static void read_bin_goto_object(std::istream &in, symbol_table_baset &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
static std::optional< 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.
#define widen_if_needed(s)