cprover
Loading...
Searching...
No Matches
goto_trace_provider.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Interface for returning Goto Traces from Goto Checkers
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
13#define CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
14
15#include <util/irep.h>
16
17class goto_tracet;
18class namespacet;
19
22class goto_trace_providert
23{
24public:
28 virtual goto_tracet build_full_trace() const = 0;
29
31 virtual goto_tracet build_shortest_trace() const = 0;
32
35 virtual goto_tracet build_trace(const irep_idt &property_id) const = 0;
36
38 virtual const namespacet &get_namespace() const = 0;
39
40 virtual ~goto_trace_providert() = default;
41};
42
43#endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
goto_trace_providert
An implementation of incremental_goto_checkert may implement this interface to provide goto traces.
Definition goto_trace_provider.h:23
goto_trace_providert::build_shortest_trace
virtual goto_tracet build_shortest_trace() const =0
Builds and returns the trace up to the first failed property.
goto_trace_providert::get_namespace
virtual const namespacet & get_namespace() const =0
Returns the namespace associated with the traces.
goto_trace_providert::~goto_trace_providert
virtual ~goto_trace_providert()=default
goto_trace_providert::build_trace
virtual goto_tracet build_trace(const irep_idt &property_id) const =0
Builds and returns the trace for the FAILed property with the given property_id.
goto_trace_providert::build_full_trace
virtual goto_tracet build_full_trace() const =0
Builds and returns the complete trace.
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
irep_idt
dstringt irep_idt
Definition verification_result.h:16