read_goto_binary.cpp File Reference

Read Goto Programs. More...

#include "read_goto_binary.h"
#include <util/config.h>
#include <util/message.h>
#include <util/replace_symbol.h>
#include <util/tempfile.h>
#include <util/unicode.h>
#include "elf_reader.h"
#include "goto_model.h"
#include "link_goto_model.h"
#include "osx_fat_reader.h"
#include "read_bin_goto_object.h"
#include <fstream>

Include dependency graph for read_goto_binary.cpp:

Go to the source code of this file.

Functions
static 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...
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. More...
bool	is_goto_binary (const std::string &filename, message_handlert &message_handler)
static std::optional< replace_symbolt::expr_mapt >	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_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.cpp.

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() [1/2]

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

filename	the file name of the goto binary
message_handler	for diagnostics

Returns

goto model on success, {} on failure

Definition at line 39 of file read_goto_binary.cpp.

read_goto_binary() [2/2]

static bool read_goto_binary ( const std::string &  filename, symbol_tablet &  symbol_table, goto_functionst &  goto_functions, message_handlert &  message_handler  )

static

Read a goto binary from a file, but do not update config.

Parameters

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

Returns

true on failure, false on success

Definition at line 58 of file read_goto_binary.cpp.

read_object_and_link()

static std::optional<replace_symbolt::expr_mapt> read_object_and_link ( const std::string &  file_name, goto_modelt &  dest, message_handlert &  message_handler  )

static

reads an object file, and also updates config

Parameters

file_name	file name of the goto binary
dest	the goto model returned
message_handler	for diagnostics

Returns

nullopt on error, type replacements to be applied otherwise

Definition at line 264 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_names	file names of goto binaries; if empty, just returns false
[out]	dest	GOTO model to update.
	message_handler	for diagnostics

Returns

True on error, false otherwise

Definition at line 280 of file read_goto_binary.cpp.