cprover
fault_localization.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fault Localization
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_FAULT_LOCALIZATION_H
13 #define CPROVER_CBMC_FAULT_LOCALIZATION_H
14 
15 #include <util/namespace.h>
16 #include <util/options.h>
17 #include <util/threeval.h>
18 
20 
21 #include "bmc.h"
22 #include "all_properties_class.h"
23 
25  public bmc_all_propertiest
26 {
27 public:
29  const goto_functionst &_goto_functions,
30  bmct &_bmc,
31  const optionst &_options)
32  :
33  bmc_all_propertiest(_goto_functions, _bmc.prop_conv, _bmc),
34  goto_functions(_goto_functions),
35  bmc(_bmc),
36  options(_options)
37  {
39  }
40 
43 
44  // override bmc_all_propertiest
45  virtual void goal_covered(const cover_goalst::goalt &);
46 
47 protected:
50  const optionst &options;
51 
52  // the failed property
53  symex_target_equationt::SSA_stepst::const_iterator failed;
54 
55  // the list of localization points up to the failed property
56  struct lpointt
57  {
59  unsigned score;
60  };
61  typedef std::map<literalt, lpointt> lpointst;
62  typedef std::map<irep_idt, lpointst> lpoints_mapt;
64 
65  // this does the actual work
66  void run(irep_idt goal_id);
67 
68  // this collects the guards as lpoints
69  void collect_guards(lpointst &lpoints);
70  void freeze_guards();
71 
72  // specify an lpoint combination to check
73  typedef std::vector<tvt> lpoints_valuet;
74  bool check(const lpointst &lpoints, const lpoints_valuet &value);
75  void update_scores(lpointst &lpoints);
76 
77  // localization method: flip each point
78  void localize_linear(lpointst &lpoints);
79 
80  // localization method: TBD
81  // void localize_TBD(
82  // prop_convt &prop_conv);
83 
84  symex_target_equationt::SSA_stepst::const_iterator get_failed_property();
85 
88 
89  void report(irep_idt goal_id);
90 
91  xmlt report_xml(irep_idt goal_id);
92 
93  // override bmc_all_propertiest
94  virtual void report(const cover_goalst &cover_goals);
95 
96  // override bmc_all_propertiest
97  virtual void do_before_solving()
98  {
99  freeze_guards();
100  }
101 };
102 
103 #endif // CPROVER_CBMC_FAULT_LOCALIZATION_H
safety_checkert::resultt stop_on_fail()
goto_programt::const_targett target
Generate Equation using Symbolic Execution.
bool check(const lpointst &lpoints, const lpoints_valuet &value)
const optionst & options
xmlt report_xml(irep_idt goal_id)
fault_localizationt(const goto_functionst &_goto_functions, bmct &_bmc, const optionst &_options)
void report(irep_idt goal_id)
void update_scores(lpointst &lpoints)
safety_checkert::resultt operator()()
instructionst::const_iterator const_targett
Definition: goto_program.h:398
virtual void do_before_solving()
std::vector< tvt > lpoints_valuet
virtual void goal_covered(const cover_goalst::goalt &)
Definition: xml.h:18
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
Symbolic Execution of ANSI-C.
void run(irep_idt goal_id)
std::map< literalt, lpointt > lpointst
symex_target_equationt::SSA_stepst::const_iterator failed
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
message_handlert & get_message_handler()
Definition: message.h:153
Bounded Model Checking for ANSI-C + HDL.
std::map< irep_idt, lpointst > lpoints_mapt
const goto_functionst & goto_functions
symex_target_equationt::SSA_stepst::const_iterator get_failed_property()
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
Options.
void collect_guards(lpointst &lpoints)
void localize_linear(lpointst &lpoints)