#include <goto_symex_fault_localizer.h>

Collaboration diagram for goto_symex_fault_localizert:

Public Member Functions
	goto_symex_fault_localizert (const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation, stack_decision_proceduret &solver)

fault_location_infot	operator() (const irep_idt &failed_property_id)

Protected Types
typedef std::map< exprt, fault_location_infot::score_mapt::iterator >	localization_pointst
	A localization point is a goto instruction that is potentially at fault. More...

typedef std::vector< tvt >	localization_points_valuet

Protected Member Functions
const SSA_stept &	collect_guards (const irep_idt &failed_property_id, localization_pointst &localization_points, fault_location_infot &fault_location)
	Collects the guards as `localization_points` up to `failed_property_id` and initializes fault_location_info, and returns the SSA step of the failed property. More...

bool	check (const SSA_stept &failed_step, const localization_pointst &, const localization_points_valuet &)

void	update_scores (const localization_pointst &)

void	localize_linear (const SSA_stept &failed_step, const localization_pointst &)

Protected Attributes
const optionst &	options

ui_message_handlert &	ui_message_handler

const symex_target_equationt &	equation

stack_decision_proceduret &	solver

Detailed Description

Definition at line 25 of file goto_symex_fault_localizer.h.

Member Typedef Documentation

◆ localization_points_valuet

typedef std::vector<tvt> goto_symex_fault_localizert::localization_points_valuet

protected

Definition at line 55 of file goto_symex_fault_localizer.h.

◆ localization_pointst

typedef std::map<exprt, fault_location_infot::score_mapt::iterator> goto_symex_fault_localizert::localization_pointst

protected

A localization point is a goto instruction that is potentially at fault.

Definition at line 44 of file goto_symex_fault_localizer.h.

Constructor & Destructor Documentation

◆ goto_symex_fault_localizert()

goto_symex_fault_localizert::goto_symex_fault_localizert	(	const optionst &	options,
		ui_message_handlert &	ui_message_handler,
		const symex_target_equationt &	equation,
		stack_decision_proceduret &	solver
	)

Definition at line 20 of file goto_symex_fault_localizer.cpp.

Member Function Documentation

◆ check()

bool goto_symex_fault_localizert::check	(	const SSA_stept &	failed_step,
		const localization_pointst &	localization_points,
		const localization_points_valuet &	value
	)

protected

Definition at line 80 of file goto_symex_fault_localizer.cpp.

◆ collect_guards()

const SSA_stept & goto_symex_fault_localizert::collect_guards	(	const irep_idt &	failed_property_id,
		localization_pointst &	localization_points,
		fault_location_infot &	fault_location
	)

protected

Collects the guards as localization_points up to failed_property_id and initializes fault_location_info, and returns the SSA step of the failed property.

Definition at line 53 of file goto_symex_fault_localizer.cpp.