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:

• /home/runner/work/cbmc/cbmc/jbmc/src/jbmc/jbmc_parse_options.h
• /home/runner/work/cbmc/cbmc/jbmc/src/jbmc/jbmc_parse_options.cpp