CBMC
goto_trace_provider.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interface for returning Goto Traces from Goto Checkers
4 
5 Author: 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 
17 class goto_tracet;
18 class namespacet;
19 
22 class goto_trace_providert
23 {
24 public:
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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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::~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_trace_providert::get_namespace
virtual const namespacet & get_namespace() const =0
Returns the namespace associated with the traces.
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:94