#include <java_multi_path_symex_checker.h>

Inheritance diagram for java_multi_path_symex_checkert:

Collaboration diagram for java_multi_path_symex_checkert:

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

goto_tracet	build_full_trace () const override
	Builds and returns the complete trace. More...

goto_tracet	build_trace (const irep_idt &property_id) const override
	Builds and returns the trace for the FAILed property with the given `property_id`. More...

goto_tracet	build_shortest_trace () const override
	Builds and returns the trace up to the first failed property. More...

Public Member Functions inherited from multi_path_symex_checkert
	multi_path_symex_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...

const namespacet &	get_namespace () const override
	Returns the namespace associated with the traces. More...

void	output_error_witness (const goto_tracet &) override

void	output_proof () override

fault_location_infot	localize_fault (const irep_idt &property_id) const override
	Returns the most likely fault locations for the given FAILed `property_id`. More...

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

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

Public Member Functions inherited from goto_trace_providert
virtual	~goto_trace_providert ()=default

Public Member Functions inherited from witness_providert
virtual	~witness_providert ()=default

Public Member Functions inherited from fault_localization_providert
virtual	~fault_localization_providert ()=default

Additional Inherited Members
Protected Member Functions inherited from multi_path_symex_checkert
virtual std::chrono::duration< double >	prepare_property_decider (propertiest &properties)
	Prepare the property decider for solving. More...

virtual void	run_property_decider (incremental_goto_checkert::resultt &result, propertiest &properties, std::chrono::duration< double > solver_runtime)
	Run the property decider, which calls the SAT solver, and set the status of checked `properties` accordingly. More...

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_checkert
bool	equation_generated

goto_symex_property_decidert	property_decider

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

Definition at line 19 of file java_multi_path_symex_checker.h.

Constructor & Destructor Documentation

◆ java_multi_path_symex_checkert()

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

inline

Definition at line 22 of file java_multi_path_symex_checker.h.

Member Function Documentation

◆ build_full_trace()

goto_tracet java_multi_path_symex_checkert::build_full_trace ( ) const

overridevirtual

Builds and returns the complete trace.

Note: If slicing is used then the trace will not be complete. E.g. with simple-slice it will end at the last assertion.

Reimplemented from multi_path_symex_checkert.

Definition at line 14 of file java_multi_path_symex_checker.cpp.

◆ build_shortest_trace()

goto_tracet java_multi_path_symex_checkert::build_shortest_trace ( ) const

overridevirtual

Builds and returns the trace up to the first failed property.

Reimplemented from multi_path_symex_checkert.

Definition at line 31 of file java_multi_path_symex_checker.cpp.

◆ build_trace()

goto_tracet java_multi_path_symex_checkert::build_trace ( const irep_idt & property_id ) const

overridevirtual

Builds and returns the trace for the FAILed property with the given property_id.

Reimplemented from multi_path_symex_checkert.

Definition at line 23 of file java_multi_path_symex_checker.cpp.

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

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

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ java_multi_path_symex_checkert()

Member Function Documentation

◆ build_full_trace()

◆ build_shortest_trace()

◆ build_trace()