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 <util/config.h>
#include "goto_model.h"
#include "link_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:

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)

bool	read_object_and_link (const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
	reads an object file More...

bool	read_object_and_link (const std::string &file_name, symbol_tablet &dest_symbol_table, goto_functionst &dest_functions, 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()

bool is_goto_binary ( const std::string & filename )

Definition at line 134 of file read_goto_binary.cpp.

References osx_fat_readert::has_gb(), elf_readert::has_section(), is_osx_fat_magic(), and widen().

Referenced by compilet::add_files_from_archive(), detect_file_type(), cbmc_parse_optionst::doit(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), lazy_goto_modelt::initialize(), and initialize_goto_model().

◆ read_goto_binary() [1/2]

bool read_goto_binary	(	const std::string &	filename,
		goto_modelt &	dest,
		message_handlert &	message_handler
	)

Definition at line 30 of file read_goto_binary.cpp.

References goto_modelt::goto_functions, message_handler, read_goto_binary(), and goto_modelt::symbol_table.

Referenced by linker_script_merget::add_linker_script_definitions(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), goto_instrument_parse_optionst::get_goto_program(), read_goto_binary(), and read_object_and_link().

◆ read_goto_binary() [2/2]

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

Definition at line 39 of file read_goto_binary.cpp.

References messaget::eom(), messaget::error(), osx_fat_readert::extract_gb(), osx_fat_readert::has_gb(), is_osx_fat_magic(), message_handler, elf_readert::number_of_sections, read_bin_goto_object(), elf_readert::section_name(), elf_readert::section_offset(), and widen().

◆ read_object_and_link() [1/2]

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

reads an object file

parameters: a file_name

Returns: true on error, false otherwise

Definition at line 198 of file read_goto_binary.cpp.

References config, messaget::eom(), link_goto_model(), message_handler, read_goto_binary(), configt::set_from_symbol_table(), messaget::statistics(), and goto_modelt::symbol_table.

Referenced by lazy_goto_modelt::initialize(), initialize_goto_model(), compilet::link(), and read_object_and_link().

◆ read_object_and_link() [2/2]

bool read_object_and_link	(	const std::string &	file_name,
		symbol_tablet &	dest_symbol_table,
		goto_functionst &	dest_functions,
		message_handlert &	message_handler
	)