12 #ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
13 #define CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
43 typedef std::map<exprt, fault_location_infot::score_mapt::iterator>
Single SSA step in the equation.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
ui_message_handlert & ui_message_handler
bool check(const SSA_stept &failed_step, const localization_pointst &, const localization_points_valuet &)
std::map< exprt, fault_location_infot::score_mapt::iterator > localization_pointst
A localization point is a goto instruction that is potentially at fault.
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)
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_in...
stack_decision_proceduret & solver
void update_scores(const localization_pointst &)
void localize_linear(const SSA_stept &failed_step, const localization_pointst &)
const symex_target_equationt & equation
std::vector< tvt > localization_points_valuet
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Interface for Goto Checkers to provide Fault Localization.
Decision procedure with incremental solving with contexts and assumptions.
Generate Equation using Symbolic Execution.