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  const lpoints_valuet &value);
77 
78  // localization method: flip each point
79  void localize_linear(lpointst &lpoints);
80 
81  // localization method: TBD
82  // void localize_TBD(
83  // prop_convt &prop_conv);
84 
85  symex_target_equationt::SSA_stepst::const_iterator get_failed_property();
86 
89 
90  void report(irep_idt goal_id);
91 
92  xmlt report_xml(irep_idt goal_id);
93 
94  // override bmc_all_propertiest
95  virtual void report(const cover_goalst &cover_goals);
96 
97  // override bmc_all_propertiest
98  virtual void do_before_solving()
99  {
100  freeze_guards();
101  }
102 };
103 
104 #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)
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
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 update_scores(lpointst &lpoints, const lpoints_valuet &value)
void localize_linear(lpointst &lpoints)