initialize_goto_model.cpp File Reference

Get a Goto Program. More...

#include "initialize_goto_model.h"
#include <util/arith_tools.h>
#include <util/c_types.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 <ansi-c/goto-conversion/goto_convert_functions.h>
#include <langapi/language.h>
#include <langapi/language_file.h>
#include <langapi/mode.h>
#include <linking/static_lifetime_init.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)
void	update_max_malloc_size (goto_modelt &goto_model, message_handlert &message_handler)
	Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed. More...

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 36 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 63 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 175 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.

Parameters

language_files	Language parsing and type checking facilities.
symbol_table	Symbol table for mode lookup and removal of an existing entry point.
unload	Functor to remove an existing entry point.
options	Configuration options.
try_mode_lookup	Try to infer the entry point's mode from the symbol table.
message_handler	Message handler.

Definition at line 114 of file initialize_goto_model.cpp.

update_max_malloc_size()

void update_max_malloc_size	(	goto_modelt &	goto_model,
		message_handlert &	message_handler
	)

Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed.

Definition at line 243 of file initialize_goto_model.cpp.