cprover
|
Read Goto Programs. More...
#include "read_goto_binary.h"
#include <fstream>
#include <unordered_set>
#include <util/message.h>
#include <util/unicode.h>
#include <util/tempfile.h>
#include <util/rename_symbol.h>
#include <util/base_type.h>
#include <langapi/language_ui.h>
#include <linking/linking_class.h>
#include "goto_model.h"
#include "read_bin_goto_object.h"
#include "elf_reader.h"
#include "osx_fat_reader.h"
Go to the source code of this file.
Functions | |
bool | read_goto_binary (const std::string &filename, goto_modelt &dest, message_handlert &message_handler) |
bool | read_goto_binary (const std::string &filename, symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler) |
bool | is_goto_binary (const std::string &filename) |
static void | rename_symbols_in_function (goto_functionst::goto_functiont &function, const rename_symbolt &rename_symbol) |
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) |
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 More... | |
bool | read_object_and_link (const std::string &file_name, goto_modelt &goto_model, message_handlert &message_handler) |
reads an object file More... | |
Read Goto Programs.
Definition in file read_goto_binary.cpp.
bool is_goto_binary | ( | const std::string & | filename | ) |
Definition at line 155 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_input_file(), compilet::find_library(), goto_diff_parse_optionst::get_goto_program(), clobber_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), and initialize_goto_model().
|
static |
Definition at line 230 of file read_goto_binary.cpp.
References base_type_eq(), rename_symbolt::expr_map, replace_symbolt::expr_map, Forall_goto_functions, Forall_goto_program_instructions, forall_symbols, goto_functions_templatet< bodyT >::function_map, symbol_exprt::get_identifier(), irept::id(), rename_symbolt::insert_expr(), namespacet::lookup(), symbolt::name, rename_symbols_in_function(), symbol_tablet::symbols, to_symbol_expr(), symbolt::type, and symbolt::value.
Referenced by read_object_and_link().
bool read_goto_binary | ( | const std::string & | filename, |
goto_modelt & | dest, | ||
message_handlert & | message_handler | ||
) |
Definition at line 41 of file read_goto_binary.cpp.
References goto_modelt::goto_functions, read_goto_binary(), and goto_modelt::symbol_table.
Referenced by goto_fence_inserter_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), clobber_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), read_goto_binary(), and read_object_and_link().
bool read_goto_binary | ( | const std::string & | filename, |
symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
message_handlert & | message_handler | ||
) |
Definition at line 50 of file read_goto_binary.cpp.
References messaget::eom(), messaget::error(), osx_fat_readert::extract_gb(), get_temporary_file(), osx_fat_readert::has_gb(), is_osx_fat_magic(), elf_readert::number_of_sections, read_bin_goto_object(), elf_readert::section_name(), elf_readert::section_offset(), and widen().
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
Definition at line 345 of file read_goto_binary.cpp.
References messaget::eom(), forall_symbols, goto_modelt::goto_functions, link_functions(), linking(), linkingt::object_type_updates, read_goto_binary(), linkingt::rename_symbol, messaget::statistics(), goto_modelt::symbol_table, symbol_tablet::symbols, and typecheckt::typecheck_main().
Referenced by cbmc_parse_optionst::get_goto_program(), initialize_goto_model(), compilet::link(), and read_object_and_link().
bool read_object_and_link | ( | const std::string & | file_name, |
goto_modelt & | goto_model, | ||
message_handlert & | message_handler | ||
) |
reads an object file
Definition at line 392 of file read_goto_binary.cpp.
References goto_modelt::goto_functions, read_object_and_link(), and goto_modelt::symbol_table.
|
static |
Definition at line 216 of file read_goto_binary.cpp.
References Forall_goto_program_instructions.
Referenced by link_functions().