Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration. More...

#include <single_loop_incremental_symex_checker.h>

Inheritance diagram for single_loop_incremental_symex_checkert:

Collaboration diagram for single_loop_incremental_symex_checkert:

Public Member Functions
	single_loop_incremental_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_trace (const irep_idt &) 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.

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

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 goto_trace_providert
virtual	~goto_trace_providert ()=default

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

Protected Attributes
abstract_goto_modelt &	goto_model

symbol_tablet	symex_symbol_table

namespacet	ns

symex_target_equationt	equation

path_fifot	path_storage

guard_managert	guard_manager

unwindsett	unwindset

symex_bmc_incremental_one_loopt	symex

bool	initial_equation_generated = false

bool	full_equation_generated = false

bool	current_equation_converted = false

goto_symex_property_decidert	property_decider

Protected Attributes inherited from incremental_goto_checkert
const optionst &	options

ui_message_handlert &	ui_message_handler

messaget	log

Additional Inherited Members
Protected Member Functions inherited from incremental_goto_checkert
	incremental_goto_checkert (const optionst &, ui_message_handlert &)

Detailed Description

Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration.

Definition at line 31 of file single_loop_incremental_symex_checker.h.

Constructor & Destructor Documentation

◆ single_loop_incremental_symex_checkert()

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

Definition at line 23 of file single_loop_incremental_symex_checker.cpp.

Member Function Documentation

◆ build_full_trace()

goto_tracet single_loop_incremental_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 191 of file single_loop_incremental_symex_checker.cpp.

◆ build_shortest_trace()

goto_tracet single_loop_incremental_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 204 of file single_loop_incremental_symex_checker.cpp.

◆ build_trace()

goto_tracet single_loop_incremental_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 220 of file single_loop_incremental_symex_checker.cpp.

◆ get_namespace()

const namespacet & single_loop_incremental_symex_checkert::get_namespace ( ) const

overridevirtual

Returns the namespace associated with the traces.

Implements goto_trace_providert.

Definition at line 234 of file single_loop_incremental_symex_checker.cpp.

◆ operator()()

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

Note: This operator can handle shrinking and expanding sets of properties in repeated invocations.

Implements incremental_goto_checkert.

Definition at line 69 of file single_loop_incremental_symex_checker.cpp.