CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
goto_symex_fault_localizer.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Fault Localization for Goto Symex
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
13#define CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
14
15#include <util/threeval.h>
16
18
19class optionst;
22class SSA_stept;
24
26{
27public:
29 const optionst &options,
33
35
36protected:
41
43 typedef std::map<exprt, fault_location_infot::score_mapt::iterator>
45
53
54 // specify a localization point combination to check
55 typedef std::vector<tvt> localization_points_valuet;
56 bool check(
60
62
63 // localization method: flip each point
64 void
66};
67
68#endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
Single SSA step in the equation.
Definition ssa_step.h:47
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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.
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
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.