An implementation of incremental_goto_checkert may implement this interface to provide goto traces.
More...
#include <goto_trace_provider.h>
Inheritance diagram for goto_trace_providert:Public Member Functions | |
| virtual goto_tracet | build_full_trace () const =0 |
| Builds and returns the complete trace. More... | |
| virtual goto_tracet | build_shortest_trace () const =0 |
| Builds and returns the trace up to the first failed property. More... | |
| 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. More... | |
| virtual const namespacet & | get_namespace () const =0 |
| Returns the namespace associated with the traces. More... | |
| virtual | ~goto_trace_providert ()=default |
Detailed Description
An implementation of incremental_goto_checkert may implement this interface to provide goto traces.
Definition at line 22 of file goto_trace_provider.h.
Constructor & Destructor Documentation
◆ ~goto_trace_providert()
|
virtualdefault |
Member Function Documentation
◆ build_full_trace()
|
pure virtual |
Builds and returns the complete trace.
- Note
- If slicing is used then the trace will not be complete. E.g. with simple-slice it will end at the last assertion.
Implemented in single_path_symex_checkert, single_loop_incremental_symex_checkert, multi_path_symex_checkert, java_single_path_symex_checkert, and java_multi_path_symex_checkert.
◆ build_shortest_trace()
|
pure virtual |
Builds and returns the trace up to the first failed property.
Implemented in single_path_symex_checkert, single_loop_incremental_symex_checkert, multi_path_symex_checkert, java_single_path_symex_checkert, and java_multi_path_symex_checkert.
◆ build_trace()
|
pure virtual |
Builds and returns the trace for the FAILed property with the given property_id.
Implemented in java_single_path_symex_checkert, java_multi_path_symex_checkert, single_path_symex_checkert, single_loop_incremental_symex_checkert, and multi_path_symex_checkert.
◆ get_namespace()
|
pure virtual |
Returns the namespace associated with the traces.
Implemented in single_path_symex_checkert, single_loop_incremental_symex_checkert, and multi_path_symex_checkert.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/goto-checker/goto_trace_provider.h
