cprover
jbmc_parse_optionst Class Reference

#include <jbmc_parse_options.h>

+ Inheritance diagram for jbmc_parse_optionst:
+ Collaboration diagram for jbmc_parse_optionst:

Public Member Functions

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)
 
- Public Member Functions inherited from parse_options_baset
 parse_options_baset (const std::string &optstring, int argc, const char **argv, const std::string &program)
 
virtual void usage_error ()
 
virtual int main ()
 
virtual ~parse_options_baset ()
 

Static Public Member Functions

static void set_default_options (optionst &)
 Set the options that have default values. More...
 

Protected Member Functions

void get_command_line_options (optionst &)
 
int get_goto_program (std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
 
bool show_loaded_functions (const abstract_goto_modelt &goto_model)
 
bool show_loaded_symbols (const abstract_goto_modelt &goto_model)
 

Protected Attributes

java_object_factory_parameterst object_factory_params
 
bool stub_objects_are_not_null
 
std::unique_ptr< class_hierarchytclass_hierarchy
 
- Protected Attributes inherited from parse_options_baset
ui_message_handlert ui_message_handler
 
messaget log
 

Additional Inherited Members

- Public Attributes inherited from parse_options_baset
cmdlinet cmdline
 

Detailed Description

Definition at line 91 of file jbmc_parse_options.h.

Constructor & Destructor Documentation

◆ jbmc_parse_optionst() [1/2]

jbmc_parse_optionst::jbmc_parse_optionst ( int  argc,
const char **  argv 
)

Definition at line 77 of file jbmc_parse_options.cpp.

◆ jbmc_parse_optionst() [2/2]

jbmc_parse_optionst::jbmc_parse_optionst ( int  argc,
const char **  argv,
const std::string &  extra_options 
)

Definition at line 88 of file jbmc_parse_options.cpp.

Member Function Documentation

◆ can_generate_function_body()

bool jbmc_parse_optionst::can_generate_function_body ( const irep_idt name)

Definition at line 971 of file jbmc_parse_options.cpp.

◆ doit()

int jbmc_parse_optionst::doit ( )
overridevirtual

invoke main modules

Implements parse_options_baset.

Definition at line 425 of file jbmc_parse_options.cpp.

◆ generate_function_body()

bool jbmc_parse_optionst::generate_function_body ( const irep_idt function_name,
symbol_table_baset symbol_table,
goto_functiont function,
bool  body_available 
)

Definition at line 978 of file jbmc_parse_options.cpp.

◆ get_command_line_options()

void jbmc_parse_optionst::get_command_line_options ( optionst options)
protected

Definition at line 122 of file jbmc_parse_options.cpp.

◆ get_goto_program()

int jbmc_parse_optionst::get_goto_program ( std::unique_ptr< abstract_goto_modelt > &  goto_model,
const optionst options 
)
protected

Definition at line 664 of file jbmc_parse_options.cpp.

◆ help()

void jbmc_parse_optionst::help ( )
overridevirtual

display command line help

Reimplemented from parse_options_baset.

Definition at line 1014 of file jbmc_parse_options.cpp.

◆ process_goto_function()

void jbmc_parse_optionst::process_goto_function ( goto_model_functiont function,
const abstract_goto_modelt model,
const optionst options 
)

Definition at line 740 of file jbmc_parse_options.cpp.

◆ process_goto_functions()

bool jbmc_parse_optionst::process_goto_functions ( goto_modelt goto_model,
const optionst options 
)

Definition at line 877 of file jbmc_parse_options.cpp.

◆ 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 102 of file jbmc_parse_options.cpp.

◆ show_loaded_functions()

bool jbmc_parse_optionst::show_loaded_functions ( const abstract_goto_modelt goto_model)
protected

Definition at line 845 of file jbmc_parse_options.cpp.

◆ show_loaded_symbols()

bool jbmc_parse_optionst::show_loaded_symbols ( const abstract_goto_modelt goto_model)
protected

Definition at line 828 of file jbmc_parse_options.cpp.

Member Data Documentation

◆ class_hierarchy

std::unique_ptr<class_hierarchyt> jbmc_parse_optionst::class_hierarchy
protected

Definition at line 127 of file jbmc_parse_options.h.

◆ object_factory_params

java_object_factory_parameterst jbmc_parse_optionst::object_factory_params
protected

Definition at line 124 of file jbmc_parse_options.h.

◆ stub_objects_are_not_null

bool jbmc_parse_optionst::stub_objects_are_not_null
protected

Definition at line 125 of file jbmc_parse_options.h.


The documentation for this class was generated from the following files: