Inheritance diagram for multi_path_symex_only_checkert:

Collaboration diagram for multi_path_symex_only_checkert:

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

Protected Member Functions
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
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

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

void multi_path_symex_only_checkert::generate_equation ( )

protectedvirtual

Generates the equation by running goto-symex.

incremental_goto_checkert::resultt multi_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.