cprover
|
Initialize a Goto Program. More...
Go to the source code of this file.
Functions | |
goto_modelt | initialize_goto_model (const cmdlinet &cmdline, message_handlert &message_handler) |
Initialize a Goto Program.
Definition in file initialize_goto_model.h.
goto_modelt initialize_goto_model | ( | const cmdlinet & | cmdline, |
message_handlert & | message_handler | ||
) |
Definition at line 29 of file initialize_goto_model.cpp.
References language_filest::add_file(), cmdlinet::args, config, goto_functionst::entry_point(), messaget::eom(), messaget::error(), language_filest::final(), language_filest::generate_support_functions(), get_language_from_filename(), languaget::get_language_options(), messaget::get_message_handler(), language_filet::get_modules(), goto_convert(), goto_modelt::goto_functions, symbol_table_baset::has_symbol(), is_goto_binary(), cmdlinet::isset(), language_filet::language, message_handler, languaget::parse(), read_object_and_link(), source_locationt::set_file(), messaget::set_message_handler(), configt::set_object_bits_from_symbol_table(), language_filest::set_should_generate_opaque_method_stubs(), messaget::mstreamt::source_location, messaget::status(), goto_modelt::symbol_table, language_filest::typecheck(), and widen().
Referenced by clobber_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), and cbmc_parse_optionst::get_goto_program().