cprover
|
Initialize command line arguments. More...
Go to the source code of this file.
Functions | |
bool | model_argc_argv (goto_modelt &, unsigned max_argc, message_handlert &) |
Set up argv with up to max_argc pointers into an array of 4096 bytes. More... | |
Initialize command line arguments.
Definition in file model_argc_argv.h.
bool model_argc_argv | ( | goto_modelt & | goto_model, |
unsigned | max_argc, | ||
message_handlert & | message_handler | ||
) |
Set up argv with up to max_argc pointers into an array of 4096 bytes.
symbol_table | Input program's symbol table |
goto_functions | Input program's intermediate representation |
max_argc | User-specified maximum number of arguments to be modelled |
message_handler | message logging |
Definition at line 39 of file model_argc_argv.cpp.
References symbol_table_baset::add(), configt::ansi_c, config, CPROVER_PREFIX, DATA_INVARIANT, goto_functionst::entry_point(), messaget::eom(), messaget::error(), Forall_goto_program_instructions, code_function_callt::function(), goto_functionst::function_map, symbol_exprt::get_identifier(), goto_convert(), goto_modelt::goto_functions, has_prefix(), symbol_table_baset::has_symbol(), irept::id(), id2string(), replace_symbolt::insert(), goto_programt::instructions, irept::is_not_nil(), namespacet::lookup(), configt::main, message_handler, symbolt::mode, symbolt::name, configt::ansi_ct::NONE, code_typet::parameters(), POSTCONDITION, configt::ansi_ct::preprocessor, remove_skip(), messaget::set_message_handler(), goto_modelt::symbol_table, symbol_table_baset::symbols, to_code(), to_code_function_call(), to_code_type(), to_symbol_expr(), symbolt::type, UNREACHABLE, and messaget::warning().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().