java_multi_path_symex_checkert Class Reference

#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.
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.
goto_tracet	build_shortest_trace () const override
	Builds and returns the trace up to the first failed property.
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.
goto_tracet	build_full_trace () const override
	Builds and returns the complete trace.
goto_tracet	build_shortest_trace () const override
	Builds and returns the trace up to the first failed property.
goto_tracet	build_trace (const irep_idt &) const override
	Builds and returns the trace for the FAILed property with the given property_id.
const namespacet &	get_namespace () const override
	Returns the namespace associated with the traces.
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.
void	report () override
	Additional reporting that may result from the underlying solver, no-op by default.
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.
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.
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.
Protected Member Functions inherited from multi_path_symex_only_checkert
virtual void	generate_equation ()
	Generates the equation by running goto-symex.
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.
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.

Implements goto_trace_providert.

Definition at line 12 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.

Implements goto_trace_providert.

Definition at line 29 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.

Implements goto_trace_providert.

Definition at line 21 of file java_multi_path_symex_checker.cpp.

---

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

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