cprover
read_goto_binary.cpp File Reference

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_modeltread_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...
 

Detailed Description

Read Goto Programs.

Definition in file read_goto_binary.cpp.

Function Documentation

◆ is_goto_binary()

bool is_goto_binary ( const std::string &  filename)

Definition at line 168 of file read_goto_binary.cpp.

◆ read_goto_binary() [1/3]

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.

Parameters
filenamethe file name of the goto binary
destthe goto model returned
message_handlerfor diagnostics
Deprecated:
Use read_goto_binary(file, message_handler) instead
Returns
true on failure, false on success

Definition at line 36 of file read_goto_binary.cpp.

◆ read_goto_binary() [2/3]

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.

Parameters
filenamethe file name of the goto binary
message_handlerfor diagnostics
Returns
goto model on success, {} on failure

Definition at line 50 of file read_goto_binary.cpp.

◆ read_goto_binary() [3/3]

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.

Parameters
filenamethe file name of the goto binary
symbol_tablethe symbol table from the goto binary
goto_functionsthe goto functions from the goto binary
message_handlerfor diagnostics
Returns
true on failure, false on success

Definition at line 69 of file read_goto_binary.cpp.

◆ read_object_and_link() [1/2]

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

Parameters
file_namefile name of the goto binary
destthe goto model returned
message_handlerfor diagnostics
Returns
true on error, false otherwise

Definition at line 234 of file read_goto_binary.cpp.

◆ read_object_and_link() [2/2]

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

Parameters
file_namefile name of the goto binary
dest_symbol_tablesymbol table to update
dest_functionscollection of goto functions to update
message_handlerfor diagnostics
Returns
true on error, false otherwise

Definition at line 272 of file read_goto_binary.cpp.