Skip to content

Commit 35fbdab

Browse files
Add fault localization provider interface
Can be implemented by an incremental goto checker to provide information about the likely fault location.
1 parent 05b2bb2 commit 35fbdab

File tree

1 file changed

+41
-0
lines changed

1 file changed

+41
-0
lines changed
Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
/*******************************************************************\
2+
3+
Module: Interface for Goto Checkers to provide Fault Localization
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Interface for Goto Checkers to provide Fault Localization
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+
28+
/// An implementation of `incremental_goto_checkert`
29+
/// may implement this interface to provide fault localization information.
30+
class fault_localization_providert
31+
{
32+
public:
33+
/// Returns the most likely fault locations
34+
/// for the given FAILed \p property_id
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

0 commit comments

Comments
 (0)