Uses goto-symex to generate a symex_target_equationt for each path. More...

#include <single_path_symex_only_checker.h>

Inheritance diagram for single_path_symex_only_checkert:

Collaboration diagram for single_path_symex_only_checkert:

Public Member Functions
	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.

Protected Member Functions
void	equation_output (const symex_bmct &symex, const symex_target_equationt &equation)
virtual void	setup_symex (symex_bmct &symex)
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	is_ready_to_decide (const symex_bmct &symex, const path_storaget::patht &path)
	Returns whether the given `path` produced by `symex` is ready to be checked.
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
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

Uses goto-symex to generate a symex_target_equationt for each path.

Definition at line 26 of file single_path_symex_only_checker.h.

Constructor & Destructor Documentation

◆ single_path_symex_only_checkert()

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

Definition at line 24 of file single_path_symex_only_checker.cpp.

◆ ~single_path_symex_only_checkert()

virtual single_path_symex_only_checkert::~single_path_symex_only_checkert ( )

virtualdefault

Member Function Documentation

◆ equation_output()

void single_path_symex_only_checkert::equation_output	(	const symex_bmct &	symex,
		const symex_target_equationt &	equation )

protected

Definition at line 130 of file single_path_symex_only_checker.cpp.

◆ final_update_properties()

void single_path_symex_only_checkert::final_update_properties	(	propertiest &	properties,
		std::unordered_set< irep_idt > &	updated_properties )

protectedvirtual

Updates the properties after having finished exploration and adds their property IDs to updated_properties.

Definition at line 167 of file single_path_symex_only_checker.cpp.

◆ has_finished_exploration()

bool single_path_symex_only_checkert::has_finished_exploration ( const propertiest & properties )

protectedvirtual

Returns whether we should stop exploring paths.

Definition at line 87 of file single_path_symex_only_checker.cpp.

◆ initialize_worklist()

void single_path_symex_only_checkert::initialize_worklist ( )

protectedvirtual

Adds the initial goto-symex state as a path to the worklist.

Definition at line 65 of file single_path_symex_only_checker.cpp.

◆ is_ready_to_decide()

bool single_path_symex_only_checkert::is_ready_to_decide	(	const symex_bmct &	symex,
		const path_storaget::patht &	path )

protectedvirtual

Returns whether the given path produced by symex is ready to be checked.

Reimplemented in single_path_symex_checkert.

Definition at line 122 of file single_path_symex_only_checker.cpp.

◆ operator()()

incremental_goto_checkert::resultt single_path_symex_only_checkert::operator() ( propertiest & properties )

overridevirtual

Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by incremental_goto_checkert hold.

Parameters

[out] properties Properties updated to whether their status have been determined. Newly discovered properties are added.

Returns: whether the goto checker found a violated property (FOUND_FAIL) or whether it is DONE with the given properties, together with the properties whose status changed since the last call to operator(). After returning DONE, another call to operator() with the same properties will return DONE and leave the properties' status unchanged. If there is a property with status FAIL then its counterexample can be retrieved by calling build_error_trace before any subsequent call to operator(). incremental_goto_checkert derivatives shall be implemented in a way such that repeated calls to operator() shall return when the next FAILed property has been found until eventually it does not find any failing properties any more.

Implements incremental_goto_checkert.

Definition at line 39 of file single_path_symex_only_checker.cpp.

◆ resume_path()

bool single_path_symex_only_checkert::resume_path ( path_storaget::patht & path )

protectedvirtual

Continues exploring the given path using goto-symex.

Returns: whether the path is ready to be checked

Definition at line 95 of file single_path_symex_only_checker.cpp.

◆ setup_symex()

virtual void single_path_symex_only_checkert::setup_symex ( symex_bmct & symex )

inlineprotectedvirtual

Reimplemented in java_single_path_symex_checkert, and java_single_path_symex_only_checkert.

Definition at line 51 of file single_path_symex_only_checker.h.

◆ update_properties()

void single_path_symex_only_checkert::update_properties	(	propertiest &	properties,
		std::unordered_set< irep_idt > &	updated_properties,
		const symex_target_equationt &	equation )