Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert. More...

Inheritance diagram for all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >:

Collaboration diagram for all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >:

Public Member Functions
	all_properties_verifier_with_fault_localizationt (const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)

resultt	operator() () override
	Check whether all properties hold. More...

void	report () override
	Report results. More...

const goto_trace_storaget &	get_traces () const

Public Member Functions inherited from goto_verifiert
	goto_verifiert ()=delete

	goto_verifiert (const goto_verifiert &)=delete

virtual	~goto_verifiert ()=default

const propertiest &	get_properties ()
	Returns the properties. More...

Protected Attributes
abstract_goto_modelt &	goto_model

incremental_goto_checkerT	incremental_goto_checker

std::size_t	iterations = 1

goto_trace_storaget	traces

std::unordered_map< irep_idt, fault_location_infot >	fault_locations

Protected Attributes inherited from goto_verifiert
const optionst &	options

ui_message_handlert &	ui_message_handler

messaget	log

propertiest	properties

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

Detailed Description

Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.

Constructor & Destructor Documentation

template<class incremental_goto_checkerT >

all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >::all_properties_verifier_with_fault_localizationt	(	const optionst &	options,
		ui_message_handlert &	ui_message_handler,
		abstract_goto_modelt &	goto_model
	)

inline

template<class incremental_goto_checkerT >

const goto_trace_storaget& all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >::get_traces ( ) const

inline

template<class incremental_goto_checkerT >

resultt all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >::operator() ( )

inlineoverridevirtual

Check whether all properties hold.

Returns: PASS if all properties are PASS, FAIL if at least one property is FAIL and no property is ERROR, UNKNOWN if no property is FAIL or ERROR and at least one property is UNKNOWN, ERROR if at least one property is error.