CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
fault_localization_provider.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Interface for Goto Checkers to provide Fault Localization
4
5Author: 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
18
19class goto_tracet;
20class namespacet;
21
31
35{
36public:
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
An implementation of incremental_goto_checkert may implement this interface to provide fault localiza...
virtual ~fault_localization_providert()=default
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.
instructionst::const_iterator const_targett
Trace of a GOTO program.
Definition goto_trace.h:177
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Concrete Goto Program.
std::map< goto_programt::const_targett, std::size_t, goto_programt::target_less_than > score_mapt
A total order over targett and const_targett.