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 <langapi/language_ui.h>
#include <linking/linking_class.h>
#include "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)
 
bool read_goto_binary (const std::string &filename, symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
 
bool is_goto_binary (const std::string &filename)
 
static void rename_symbols_in_function (goto_functionst::goto_functiont &function, const rename_symbolt &rename_symbol)
 
static bool link_functions (symbol_tablet &dest_symbol_table, goto_functionst &dest_functions, const symbol_tablet &src_symbol_table, goto_functionst &src_functions, const rename_symbolt &rename_symbol, const std::unordered_set< irep_idt, irep_id_hash > &weak_symbols, const replace_symbolt &object_type_updates)
 
bool read_object_and_link (const std::string &file_name, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
 reads an object file More...
 
bool read_object_and_link (const std::string &file_name, goto_modelt &goto_model, message_handlert &message_handler)
 reads an object file More...
 

Detailed Description

Read Goto Programs.

Definition in file read_goto_binary.cpp.

Function Documentation

§ is_goto_binary()

§ link_functions()

§ read_goto_binary() [1/2]

§ read_goto_binary() [2/2]

§ read_object_and_link() [1/2]

bool read_object_and_link ( const std::string &  file_name,
symbol_tablet symbol_table,
goto_functionst functions,
message_handlert message_handler 
)

§ read_object_and_link() [2/2]

bool read_object_and_link ( const std::string &  file_name,
goto_modelt goto_model,
message_handlert message_handler 
)

reads an object file

parameters: a file_name
Returns
true on error, false otherwise

Definition at line 392 of file read_goto_binary.cpp.

References goto_modelt::goto_functions, read_object_and_link(), and goto_modelt::symbol_table.

§ rename_symbols_in_function()

static void rename_symbols_in_function ( goto_functionst::goto_functiont function,
const rename_symbolt rename_symbol 
)
static

Definition at line 216 of file read_goto_binary.cpp.

References Forall_goto_program_instructions.

Referenced by link_functions().