cprover
Loading...
Searching...
No Matches
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
 
virtual void help () override
 display command line help
 
 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 ()
 
void log_version_and_architecture (const std::string &front_end)
 Write version and system architecture to log.status().
 

Static Public Member Functions

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

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 Member Functions inherited from parse_options_baset
virtual void register_languages ()
 

Protected Attributes

java_object_factory_parameterst object_factory_params
 
bool stub_objects_are_not_null
 
std::unique_ptr< class_hierarchytclass_hierarchy
 
optionalt< prefix_filtertmethod_context
 See java_bytecode_languaget::method_context.
 
- 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 90 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 67 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 76 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 912 of file jbmc_parse_options.cpp.

◆ doit()

int jbmc_parse_optionst::doit ( )
overridevirtual

invoke main modules

Implements parse_options_baset.

Definition at line 376 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 919 of file jbmc_parse_options.cpp.

◆ get_command_line_options()

void jbmc_parse_optionst::get_command_line_options ( optionst & options)
protected

Definition at line 109 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 595 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 957 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 673 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 808 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 92 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 776 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 759 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 126 of file jbmc_parse_options.h.

◆ method_context

optionalt<prefix_filtert> jbmc_parse_optionst::method_context
protected

See java_bytecode_languaget::method_context.

The two fields are initialized in exactly the same way. TODO Refactor this so it only needs to be computed once, in one place.

Definition at line 138 of file jbmc_parse_options.h.

◆ object_factory_params

java_object_factory_parameterst jbmc_parse_optionst::object_factory_params
protected

Definition at line 123 of file jbmc_parse_options.h.

◆ stub_objects_are_not_null

bool jbmc_parse_optionst::stub_objects_are_not_null
protected

Definition at line 124 of file jbmc_parse_options.h.


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