#include <jbmc_parse_options.h>
|
virtual int | doit () override |
| invoke main modules More...
|
|
virtual void | help () override |
| display command line help More...
|
|
| jbmc_parse_optionst (int argc, const char **argv) |
|
| jbmc_parse_optionst (int argc, const char **argv, const std::string &extra_options) |
|
void | process_goto_function (goto_model_functiont &function, const abstract_goto_modelt &, const optionst &) |
|
bool | process_goto_functions (goto_modelt &goto_model, const optionst &options) |
|
bool | can_generate_function_body (const irep_idt &name) |
|
bool | generate_function_body (const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) |
|
| parse_options_baset (const std::string &optstring, int argc, const char **argv) |
|
virtual void | usage_error () |
|
virtual int | main () |
|
virtual | ~parse_options_baset () |
|
virtual void | set_message_handler (message_handlert &_message_handler) |
|
message_handlert & | get_message_handler () |
|
| messaget () |
|
| messaget (const messaget &other) |
|
messaget & | operator= (const messaget &other) |
|
| messaget (message_handlert &_message_handler) |
|
virtual | ~messaget () |
|
mstreamt & | get_mstream (unsigned message_level) const |
|
mstreamt & | error () const |
|
mstreamt & | warning () const |
|
mstreamt & | result () const |
|
mstreamt & | status () const |
|
mstreamt & | statistics () const |
|
mstreamt & | progress () const |
|
mstreamt & | debug () const |
|
void | conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const |
| Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream . More...
|
|
Definition at line 86 of file jbmc_parse_options.h.
◆ jbmc_parse_optionst() [1/2]
jbmc_parse_optionst::jbmc_parse_optionst |
( |
int |
argc, |
|
|
const char ** |
argv |
|
) |
| |
◆ jbmc_parse_optionst() [2/2]
jbmc_parse_optionst::jbmc_parse_optionst |
( |
int |
argc, |
|
|
const char ** |
argv, |
|
|
const std::string & |
extra_options |
|
) |
| |
◆ can_generate_function_body()
bool jbmc_parse_optionst::can_generate_function_body |
( |
const irep_idt & |
name | ) |
|
◆ doit()
int jbmc_parse_optionst::doit |
( |
| ) |
|
|
overridevirtual |
◆ generate_function_body()
◆ get_command_line_options()
void jbmc_parse_optionst::get_command_line_options |
( |
optionst & |
options | ) |
|
|
protected |
◆ get_goto_program()
int jbmc_parse_optionst::get_goto_program |
( |
std::unique_ptr< goto_modelt > & |
goto_model, |
|
|
const optionst & |
options |
|
) |
| |
|
protected |
◆ help()
void jbmc_parse_optionst::help |
( |
| ) |
|
|
overridevirtual |
◆ process_goto_function()
◆ process_goto_functions()
bool jbmc_parse_optionst::process_goto_functions |
( |
goto_modelt & |
goto_model, |
|
|
const optionst & |
options |
|
) |
| |
◆ set_default_options()
void jbmc_parse_optionst::set_default_options |
( |
optionst & |
options | ) |
|
|
static |
Set the options that have default values.
This function can be called from clients that wish to emulate JBMC's default behaviour, for example unit tests.
Definition at line 84 of file jbmc_parse_options.cpp.
◆ set_properties()
bool jbmc_parse_optionst::set_properties |
( |
goto_modelt & |
goto_model | ) |
|
|
protected |
◆ show_loaded_functions()
◆ class_hierarchy
◆ object_factory_params
◆ path_strategy_chooser
◆ stub_objects_are_not_null
bool jbmc_parse_optionst::stub_objects_are_not_null |
|
protected |
◆ ui_message_handler
The documentation for this class was generated from the following files: