cprover
|
Read Goto Programs. More...
#include <string>
Go to the source code of this file.
Functions | |
bool | read_goto_binary (const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &) |
bool | read_goto_binary (const std::string &filename, goto_modelt &dest, message_handlert &) |
bool | is_goto_binary (const std::string &filename) |
bool | read_object_and_link (const std::string &file_name, symbol_tablet &, goto_functionst &, message_handlert &) |
reads an object file More... | |
bool | read_object_and_link (const std::string &file_name, goto_modelt &, message_handlert &) |
reads an object file More... | |
Read Goto Programs.
Definition in file read_goto_binary.h.
bool is_goto_binary | ( | const std::string & | filename | ) |
Definition at line 134 of file read_goto_binary.cpp.
References osx_fat_readert::has_gb(), elf_readert::has_section(), is_osx_fat_magic(), and widen().
Referenced by compilet::add_files_from_archive(), detect_file_type(), cbmc_parse_optionst::doit(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), lazy_goto_modelt::initialize(), and initialize_goto_model().
bool read_goto_binary | ( | const std::string & | filename, |
symbol_tablet & | , | ||
goto_functionst & | , | ||
message_handlert & | |||
) |
Definition at line 39 of file read_goto_binary.cpp.
References messaget::eom(), messaget::error(), osx_fat_readert::extract_gb(), osx_fat_readert::has_gb(), is_osx_fat_magic(), message_handler, elf_readert::number_of_sections, read_bin_goto_object(), elf_readert::section_name(), elf_readert::section_offset(), and widen().
bool read_goto_binary | ( | const std::string & | filename, |
goto_modelt & | dest, | ||
message_handlert & | |||
) |
Definition at line 30 of file read_goto_binary.cpp.
References goto_modelt::goto_functions, message_handler, read_goto_binary(), and goto_modelt::symbol_table.
Referenced by linker_script_merget::add_linker_script_definitions(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), read_goto_binary(), and read_object_and_link().
bool read_object_and_link | ( | const std::string & | file_name, |
symbol_tablet & | dest_symbol_table, | ||
goto_functionst & | dest_functions, | ||
message_handlert & | message_handler | ||
) |
reads an object file
Definition at line 233 of file read_goto_binary.cpp.
References goto_modelt::goto_functions, message_handler, read_object_and_link(), symbol_tablet::swap(), goto_functionst::swap(), and goto_modelt::symbol_table.
bool read_object_and_link | ( | const std::string & | file_name, |
goto_modelt & | dest, | ||
message_handlert & | message_handler | ||
) |
reads an object file
Definition at line 198 of file read_goto_binary.cpp.
References config, messaget::eom(), link_goto_model(), message_handler, read_goto_binary(), configt::set_from_symbol_table(), messaget::statistics(), and goto_modelt::symbol_table.
Referenced by lazy_goto_modelt::initialize(), initialize_goto_model(), compilet::link(), and read_object_and_link().