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 #include <langapi/language_ui.h>
19 
21 
22 #include "bmc.h"
23 #include "all_properties_class.h"
24 
26  public bmc_all_propertiest
27 {
28 public:
30  const goto_functionst &_goto_functions,
31  bmct &_bmc,
32  const optionst &_options)
33  :
34  bmc_all_propertiest(_goto_functions, _bmc.prop_conv, _bmc),
35  goto_functions(_goto_functions),
36  bmc(_bmc),
37  options(_options)
38  {
40  }
41 
44 
45  // override bmc_all_propertiest
46  virtual void goal_covered(const cover_goalst::goalt &);
47 
48 protected:
51  const optionst &options;
52 
53  // the failed property
54  symex_target_equationt::SSA_stepst::const_iterator failed;
55 
56  // the list of localization points up to the failed property
57  struct lpointt
58  {
60  unsigned score;
61  };
62  typedef std::map<literalt, lpointt> lpointst;
63  typedef std::map<irep_idt, lpointst> lpoints_mapt;
65 
66  // this does the actual work
67  void run(irep_idt goal_id);
68 
69  // this collects the guards as lpoints
70  void collect_guards(lpointst &lpoints);
71  void freeze_guards();
72 
73  // specify an lpoint combination to check
74  typedef std::vector<tvt> lpoints_valuet;
75  bool check(const lpointst &lpoints, const lpoints_valuet &value);
76  void update_scores(lpointst &lpoints,
77  const lpoints_valuet &value);
78 
79  // localization method: flip each point
80  void localize_linear(lpointst &lpoints);
81 
82  // localization method: TBD
83  // void localize_TBD(
84  // prop_convt &prop_conv);
85 
86  symex_target_equationt::SSA_stepst::const_iterator get_failed_property();
87 
90 
91  void report(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
fault_localizationt(const goto_functionst &_goto_functions, bmct &_bmc, const optionst &_options)
void report(irep_idt goal_id)
instructionst::const_iterator const_targett
safety_checkert::resultt operator()()
virtual void do_before_solving()
std::vector< tvt > lpoints_valuet
virtual void goal_covered(const cover_goalst::goalt &)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
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:127
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()
Definition: bmc.h:32
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)