|
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 <util/config.h>#include "goto_model.h"#include "link_goto_model.h"#include "read_bin_goto_object.h"#include "elf_reader.h"#include "osx_fat_reader.h"
Include dependency graph for read_goto_binary.cpp:Go to the source code of this file.
Functions | |
| bool | read_goto_binary (const std::string &filename, goto_modelt &dest, message_handlert &message_handler) |
| Read a goto binary from a file, but do not update config. More... | |
| optionalt< goto_modelt > | read_goto_binary (const std::string &filename, message_handlert &message_handler) |
| Read a goto binary from a file, but do not update config. More... | |
| bool | read_goto_binary (const std::string &filename, symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler) |
| Read a goto binary from a file, but do not update config. More... | |
| bool | is_goto_binary (const std::string &filename) |
| 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 More... | |
| 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, and also updates the config More... | |
Read Goto Programs.
Definition in file read_goto_binary.cpp.
| bool is_goto_binary | ( | const std::string & | filename | ) |
Definition at line 168 of file read_goto_binary.cpp.
| bool read_goto_binary | ( | const std::string & | filename, |
| goto_modelt & | dest, | ||
| message_handlert & | message_handler | ||
| ) |
Read a goto binary from a file, but do not update config.
| filename | the file name of the goto binary |
| dest | the goto model returned |
| message_handler | for diagnostics |
Definition at line 36 of file read_goto_binary.cpp.
| optionalt<goto_modelt> read_goto_binary | ( | const std::string & | filename, |
| message_handlert & | message_handler | ||
| ) |
Read a goto binary from a file, but do not update config.
| filename | the file name of the goto binary |
| message_handler | for diagnostics |
Definition at line 50 of file read_goto_binary.cpp.
| bool read_goto_binary | ( | const std::string & | filename, |
| symbol_tablet & | symbol_table, | ||
| goto_functionst & | goto_functions, | ||
| message_handlert & | message_handler | ||
| ) |
Read a goto binary from a file, but do not update config.
| filename | the file name of the goto binary |
| symbol_table | the symbol table from the goto binary |
| goto_functions | the goto functions from the goto binary |
| message_handler | for diagnostics |
Definition at line 69 of file read_goto_binary.cpp.
| 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
| file_name | file name of the goto binary |
| dest | the goto model returned |
| message_handler | for diagnostics |
Definition at line 234 of file read_goto_binary.cpp.
| 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, and also updates the config
| file_name | file name of the goto binary |
| dest_symbol_table | symbol table to update |
| dest_functions | collection of goto functions to update |
| message_handler | for diagnostics |
Definition at line 272 of file read_goto_binary.cpp.