CBMC
initialize_goto_model.cpp File Reference

Get a Goto Program. More...

+ 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
sourcesCollection of input source files. No operation is performed if the collection is empty.
optionsConfiguration options.
language_filesLanguage parsing and type checking facilities.
[out]symbol_tableSymbol table to be populated.
message_handlerMessage 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_filesLanguage parsing and type checking facilities.
symbol_tableSymbol table for mode lookup and removal of an existing entry point.
unloadFunctor to remove an existing entry point.
optionsConfiguration options.
try_mode_lookupTry to infer the entry point's mode from the symbol table.
message_handlerMessage 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.