Inheritance diagram for java_multi_path_symex_only_checkert:

Collaboration diagram for java_multi_path_symex_only_checkert:

Public Member Functions
	java_multi_path_symex_only_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)

Public Member Functions inherited from multi_path_symex_only_checkert
	multi_path_symex_only_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)

resultt	operator() (propertiest &) override
	Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by `incremental_goto_checkert` hold. More...

Public Member Functions inherited from incremental_goto_checkert
	incremental_goto_checkert ()=delete

	incremental_goto_checkert (const incremental_goto_checkert &)=delete

virtual	~incremental_goto_checkert ()=default

virtual void	report ()
	Additional reporting that may result from the underlying solver, no-op by default. More...

Additional Inherited Members
Protected Member Functions inherited from multi_path_symex_only_checkert
virtual void	generate_equation ()
	Generates the equation by running goto-symex. More...

virtual void	update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
	Updates the `properties` from the `equation` and adds their property IDs to `updated_properties`. More...

Protected Member Functions inherited from incremental_goto_checkert
	incremental_goto_checkert (const optionst &, ui_message_handlert &)

Protected Attributes inherited from multi_path_symex_only_checkert
abstract_goto_modelt &	goto_model

symbol_tablet	symex_symbol_table

namespacet	ns

symex_target_equationt	equation

guard_managert	guard_manager

path_fifot	path_storage

unwindsett	unwindset

symex_bmct	symex

Protected Attributes inherited from incremental_goto_checkert
const optionst &	options

ui_message_handlert &	ui_message_handler

messaget	log

Detailed Description

Constructor & Destructor Documentation

java_multi_path_symex_only_checkert::java_multi_path_symex_only_checkert	(	const optionst &	options,
		ui_message_handlert &	ui_message_handler,
		abstract_goto_modelt &	goto_model
	)

inline

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

/home/runner/work/cbmc-documentation/cbmc-documentation/jbmc/src/java_bytecode/java_multi_path_symex_only_checker.h