Get a Goto Program. More...

#include "initialize_goto_model.h"
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/message.h>
#include <util/options.h>
#include <util/unicode.h>
#include <goto-programs/rebuild_goto_start_function.h>
#include <langapi/language.h>
#include <langapi/language_file.h>
#include <langapi/mode.h>
#include "goto_convert_functions.h"
#include "read_goto_binary.h"
#include <fstream>

Include dependency graph for initialize_goto_model.cpp:

Go to the source code of this file.

Functions
static bool	generate_entry_point_for_function (const optionst &options, symbol_tablet &symbol_table, message_handlert &message_handler)
	Generate an entry point that calls a function with the given name, based on the functions language mode in the symbol table. More...

void	initialize_from_source_files (const std::list< std::string > &sources, const optionst &options, language_filest &language_files, symbol_tablet &symbol_table, message_handlert &message_handler)
	Populate `symbol_table` from `sources` by parsing and type checking via `language_files`. More...

void	set_up_custom_entry_point (language_filest &language_files, symbol_tablet &symbol_table, const std::function< std::size_t(const irep_idt &)> &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler)
	Process the "function" option in `options` to prepare a custom entry point to replace `__CPROVER_start`. More...

goto_modelt	initialize_goto_model (const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)

Detailed Description

Get a Goto Program.

Definition in file initialize_goto_model.cpp.

Function Documentation

◆ generate_entry_point_for_function()

static bool generate_entry_point_for_function	(	const optionst &	options,
		symbol_tablet &	symbol_table,
		message_handlert &	message_handler
	)

static

Generate an entry point that calls a function with the given name, based on the functions language mode in the symbol table.

Definition at line 33 of file initialize_goto_model.cpp.

◆ initialize_from_source_files()

void initialize_from_source_files	(	const std::list< std::string > &	sources,
		const optionst &	options,
		language_filest &	language_files,
		symbol_tablet &	symbol_table,
		message_handlert &	message_handler
	)

Populate symbol_table from sources by parsing and type checking via language_files.

Throws exceptions if processing fails.

Parameters

	sources	Collection of input source files. No operation is performed if the collection is empty.
	options	Configuration options.
	language_files	Language parsing and type checking facilities.
[out]	symbol_table	Symbol table to be populated.
	message_handler	Message handler.

Definition at line 60 of file initialize_goto_model.cpp.

◆ initialize_goto_model()

goto_modelt initialize_goto_model	(	const std::vector< std::string > &	files,
		message_handlert &	message_handler,
		const optionst &	options
	)

Definition at line 172 of file initialize_goto_model.cpp.

◆ set_up_custom_entry_point()

void set_up_custom_entry_point	(	language_filest &	language_files,
		symbol_tablet &	symbol_table,
		const std::function< std::size_t(const irep_idt &)> &	unload,
		const optionst &	options,
		bool	try_mode_lookup,
		message_handlert &	message_handler
	)

Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.