12 #ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
13 #define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
22 const std::vector<std::string> &files,
35 const std::list<std::string> &sources,
54 const std::function<std::size_t(
const irep_idt &)> &unload,
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
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.
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.