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_hierarchyt > class_hierarchy
std::optional< prefix_filtert > method_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 66 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 75 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 918 of file jbmc_parse_options.cpp.

◆ doit()

int jbmc_parse_optionst::doit ( )
overridevirtual

invoke main modules

Implements parse_options_baset.

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

◆ get_command_line_options()

void jbmc_parse_optionst::get_command_line_options ( optionst & options)
protected

Definition at line 108 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 596 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 963 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 678 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 813 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 91 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 781 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 764 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

std::optional<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: