initialize_goto_model.h File Reference

Initialize a Goto Program. More...

#include "goto_model.h"

Include dependency graph for initialize_goto_model.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
goto_modelt	initialize_goto_model (const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
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...
void	update_max_malloc_size (goto_modelt &, message_handlert &)
	Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed. More...

Detailed Description

Initialize a Goto Program.

Definition in file initialize_goto_model.h.

Function Documentation

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.