cprover
goto_symex_fault_localizer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fault Localization for Goto Symex
4 
5 Author: 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/options.h>
16 #include <util/threeval.h>
17 #include <util/ui_message.h>
18 
20 
22 
24 
26 {
27 public:
29  const optionst &options,
33 
34  fault_location_infot operator()(const irep_idt &failed_property_id);
35 
36 protected:
37  const optionst &options;
41 
43  typedef std::map<exprt, fault_location_infot::score_mapt::iterator>
45 
50  const irep_idt &failed_property_id,
51  localization_pointst &localization_points,
52  fault_location_infot &fault_location);
53 
54  // specify a localization point combination to check
55  typedef std::vector<tvt> localization_points_valuet;
56  bool check(
57  const SSA_stept &failed_step,
58  const localization_pointst &,
60 
61  void update_scores(const localization_pointst &);
62 
63  // localization method: flip each point
64  void
65  localize_linear(const SSA_stept &failed_step, const localization_pointst &);
66 };
67 
68 #endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
Single SSA step in the equation.
Definition: ssa_step.h:45
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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
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.
Options.
Decision procedure with incremental solving with contexts and assumptions.
Generate Equation using Symbolic Execution.