Loading...

Searching...

No Matches

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.

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.

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

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.

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.