CBMC
read_goto_binary.h File Reference

Read Goto Programs. More...

#include <list>
#include <optional>
#include <string>
+ Include dependency graph for read_goto_binary.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

std::optional< goto_modeltread_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...
 

Detailed Description

Read Goto Programs.

Definition in file read_goto_binary.h.

Function Documentation

◆ is_goto_binary()

bool is_goto_binary ( const std::string &  filename,
message_handlert message_handler 
)

Definition at line 185 of file read_goto_binary.cpp.

◆ read_goto_binary()

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.

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

Definition at line 39 of file read_goto_binary.cpp.

◆ read_objects_and_link()

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.

Parameters
file_namesfile names of goto binaries; if empty, just returns false
[out]destGOTO model to update.
message_handlerfor diagnostics
Returns
True on error, false otherwise

Definition at line 280 of file read_goto_binary.cpp.