Go to the documentation of this file.
15 #include <unordered_set>
30 const std::string &filename,
50 return std::move(dest);
60 const std::string &filename,
83 message.error() <<
"Failed to read header from '" << filename <<
"'"
90 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
93 in, filename, symbol_table, goto_functions, message_handler);
95 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
108 in, filename, symbol_table, goto_functions, message_handler);
113 "failed to find goto-cc section in ELF binary" <<
messaget::eom;
129 if(osx_fat_reader.
has_gb())
132 if(osx_fat_reader.
extract_gb(filename, tempname()))
143 temp_in, filename, symbol_table, goto_functions, message_handler);
150 message.error() <<
"failed to find goto binary in Mach-O file"
162 osx_mach_o_readert::sectionst::const_iterator entry =
163 mach_o_reader.
sections.find(
"goto-cc");
164 if(entry != mach_o_reader.
sections.end())
166 in.seekg(entry->second.offset);
168 in, filename, symbol_table, goto_functions, message_handler);
173 <<
"failed to find goto-cc section in Mach-O binary" <<
messaget::eom;
191 const std::string &filename,
212 if(hdr[0]==0x7f && hdr[1]==
'G' && hdr[2]==
'B' && hdr[3]==
'F')
216 else if(hdr[0]==0x7f && hdr[1]==
'E' && hdr[2]==
'L' && hdr[3]==
'F')
239 if(osx_fat_reader.
has_gb())
274 const std::string &file_name,
283 if(!temp_model.has_value())
308 const std::string &file_name,
Class that provides messages with a built-in verbosity 'level'.
void link_goto_model(goto_modelt &dest, goto_modelt &src, message_handlert &message_handler)
static bool read_bin_goto_object(std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
bool has_section(const std::string &name) const
bool is_osx_mach_object(char hdr[4])
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
std::size_t number_of_sections
std::string section_name(std::size_t index) const
void set_from_symbol_table(const symbol_tablet &)
std::wstring widen(const char *s)
nonstd::optional< T > optionalt
A collection of goto functions.
bool extract_gb(const std::string &source, const std::string &dest) const
goto_functionst goto_functions
GOTO functions.
void swap(symbol_tablet &other)
Swap symbol maps between two symbol tables.
bool has_section(const std::string &name) const
static std::string binary(const constant_exprt &src)
void swap(goto_functionst &other)
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file, and also updates config
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
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_osx_fat_header(char header_bytes[8])
symbol_tablet symbol_table
Symbol table.
std::streampos section_offset(std::size_t index) const
mstreamt & statistics() const
std::string what() const override
A human readable description of what went wrong.