CBMC
fault_localization_provider.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interface for Goto Checkers to provide Fault Localization
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H
13 #define CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H
14 
15 #include <map>
16 
17 #include <goto-programs/goto_program.h>
18 
19 class goto_tracet;
20 class namespacet;
21 
22 struct fault_location_infot
23 {
24  typedef std::map<goto_programt::const_targett, std::size_t> score_mapt;
25  score_mapt scores;
26 };
27 
30 class fault_localization_providert
31 {
32 public:
35  virtual fault_location_infot
36  localize_fault(const irep_idt &property_id) const = 0;
37 
38  virtual ~fault_localization_providert() = default;
39 };
40 
41 #endif // CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
fault_localization_providert::~fault_localization_providert
virtual ~fault_localization_providert()=default
fault_location_infot
Definition: fault_localization_provider.h:22
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
fault_location_infot::scores
score_mapt scores
Definition: fault_localization_provider.h:25
fault_location_infot::score_mapt
std::map< goto_programt::const_targett, std::size_t > score_mapt
Definition: fault_localization_provider.h:24
fault_localization_providert
An implementation of incremental_goto_checkert may implement this interface to provide fault localiza...
Definition: fault_localization_provider.h:30
goto_program.h
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:174
fault_localization_providert::localize_fault
virtual fault_location_infot localize_fault(const irep_idt &property_id) const =0
Returns the most likely fault locations for the given FAILed property_id.