As more detailed histories can get complex (for example, nested loops or deep, mutually recursive call stacks) they often need some user controls or limits. More...
#include <ai_history.h>
Inheritance diagram for ai_history_factory_baset:Public Member Functions | |
| virtual ai_history_baset::trace_ptrt | epoch (ai_history_baset::locationt)=0 |
| Creates a new history from the given starting point. More... | |
| virtual | ~ai_history_factory_baset () |
Detailed Description
As more detailed histories can get complex (for example, nested loops or deep, mutually recursive call stacks) they often need some user controls or limits.
The best way to do this is to give the limits to the first, start-of-history object and let it propagate. Having a factory gives a way of wrapping this information up in a common interface
Definition at line 241 of file ai_history.h.
Constructor & Destructor Documentation
◆ ~ai_history_factory_baset()
|
inlinevirtual |
Definition at line 247 of file ai_history.h.
Member Function Documentation
◆ epoch()
|
pure virtual |
Creates a new history from the given starting point.
Implemented in local_control_flow_history_factoryt, call_stack_history_factoryt, and ai_history_factory_default_constructort< traceT >.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/analyses/ai_history.h
