CBMC
|
Read Goto Programs. More...
#include <list>
#include <optional>
#include <string>
Go to the source code of this file.
Functions | |
std::optional< goto_modelt > | read_goto_binary (const std::string &filename, message_handlert &) |
Read a goto binary from a file, but do not update config. More... | |
bool | is_goto_binary (const std::string &filename, message_handlert &) |
bool | read_objects_and_link (const std::list< std::string > &file_names, goto_modelt &dest, message_handlert &message_handler) |
Reads object files and updates the config if any files were read. More... | |
Read Goto Programs.
Definition in file read_goto_binary.h.
bool is_goto_binary | ( | const std::string & | filename, |
message_handlert & | message_handler | ||
) |
Definition at line 185 of file read_goto_binary.cpp.
std::optional<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 39 of file read_goto_binary.cpp.
bool read_objects_and_link | ( | const std::list< std::string > & | file_names, |
goto_modelt & | dest, | ||
message_handlert & | message_handler | ||
) |
Reads object files and updates the config if any files were read.
file_names | file names of goto binaries; if empty, just returns false | |
[out] | dest | GOTO model to update. |
message_handler | for diagnostics |
Definition at line 280 of file read_goto_binary.cpp.