cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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<
25
goto_programt::const_targett
,
26
std::size_t,
27
goto_programt::target_less_than
>
28
score_mapt
;
29
score_mapt
scores
;
30
};
31
34
class
fault_localization_providert
35
{
36
public
:
39
virtual
fault_location_infot
40
localize_fault
(
const
irep_idt
&property_id)
const
= 0;
41
42
virtual
~fault_localization_providert
() =
default
;
43
};
44
45
#endif
// CPROVER_GOTO_CHECKER_FAULT_LOCALIZATION_PROVIDER_H
fault_localization_providert
An implementation of incremental_goto_checkert may implement this interface to provide fault localiza...
Definition
fault_localization_provider.h:35
fault_localization_providert::~fault_localization_providert
virtual ~fault_localization_providert()=default
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.
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition
goto_program.h:614
goto_programt::target_less_than
instructiont::target_less_than target_less_than
Definition
goto_program.h:618
goto_tracet
Trace of a GOTO program.
Definition
goto_trace.h:177
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
goto_program.h
Concrete Goto Program.
fault_location_infot
Definition
fault_localization_provider.h:23
fault_location_infot::scores
score_mapt scores
Definition
fault_localization_provider.h:29
fault_location_infot::score_mapt
std::map< goto_programt::const_targett, std::size_t, goto_programt::target_less_than > score_mapt
Definition
fault_localization_provider.h:28
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-checker
fault_localization_provider.h
Generated by
1.17.0