java_single_path_symex_checkert Class Reference

#include <java_single_path_symex_checker.h>

Inheritance diagram for java_single_path_symex_checkert:

Collaboration diagram for java_single_path_symex_checkert:

Public Member Functions
	java_single_path_symex_checkert (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
void	setup_symex (symex_bmct &symex) override
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 &property_id) const override
	Builds and returns the trace for the FAILed property with the given property_id.
Public Member Functions inherited from single_path_symex_checkert
	single_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
virtual	~single_path_symex_checkert ()=default
Public Member Functions inherited from single_path_symex_only_checkert
	single_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.
virtual	~single_path_symex_only_checkert ()=default
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.
Public Member Functions inherited from witness_providert
virtual	~witness_providert ()=default
Public Member Functions inherited from goto_trace_providert
virtual	~goto_trace_providert ()=default

Additional Inherited Members
Protected Member Functions inherited from single_path_symex_checkert
bool	is_ready_to_decide (const symex_bmct &, const path_storaget::patht &) override
	Returns whether the given path produced by symex is ready to be checked.
virtual std::chrono::duration< double >	prepare_property_decider (propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider)
	Prepare the property_decider for solving.
virtual void	run_property_decider (incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, 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 single_path_symex_only_checkert
void	equation_output (const symex_bmct &symex, const symex_target_equationt &equation)
virtual void	initialize_worklist ()
	Adds the initial goto-symex state as a path to the worklist.
virtual bool	resume_path (path_storaget::patht &path)
	Continues exploring the given path using goto-symex.
virtual bool	has_finished_exploration (const propertiest &)
	Returns whether we should stop exploring paths.
virtual void	update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
	Updates the properties from the equation and adds their property IDs to updated_properties.
virtual void	final_update_properties (propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
	Updates the properties after having finished exploration 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 single_path_symex_checkert
bool	symex_initialized = false
std::unique_ptr< goto_symex_property_decidert >	property_decider
Protected Attributes inherited from single_path_symex_only_checkert
abstract_goto_modelt &	goto_model
symbol_tablet	symex_symbol_table
namespacet	ns
guard_managert	guard_manager
std::unique_ptr< path_storaget >	worklist
std::chrono::duration< double >	symex_runtime
unwindsett	unwindset
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_single_path_symex_checker.h.

Constructor & Destructor Documentation

java_single_path_symex_checkert()

java_single_path_symex_checkert::java_single_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_single_path_symex_checker.h.

Member Function Documentation

build_full_trace()

goto_tracet java_single_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_single_path_symex_checker.cpp.

build_shortest_trace()

goto_tracet java_single_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 20 of file java_single_path_symex_checker.cpp.

build_trace()

goto_tracet java_single_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 29 of file java_single_path_symex_checker.cpp.

setup_symex()

void java_single_path_symex_checkert::setup_symex ( symex_bmct &  symex )

inlineoverridevirtual

Reimplemented from single_path_symex_only_checkert.

Definition at line 30 of file java_single_path_symex_checker.h.

---

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

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