Records all local control-flow decisions up to a limit of number of histories per location. More...
#include <local_control_flow_history.h>
Collaboration diagram for local_control_flow_decisiont:Public Types | |
| typedef ai_history_baset::locationt | locationt |
| typedef std::shared_ptr< const local_control_flow_decisiont > | lcfd_ptrt |
Public Member Functions | |
| local_control_flow_decisiont (locationt loc, bool taken, lcfd_ptrt ptr) | |
| bool | operator< (const local_control_flow_decisiont &op) const |
| bool | operator== (const local_control_flow_decisiont &op) const |
Public Attributes | |
| locationt | branch_location |
| bool | branch_taken |
| lcfd_ptrt | previous |
Detailed Description
Records all local control-flow decisions up to a limit of number of histories per location.
This gives a linear scaling between history limits and space and time used. Note this does no interprocedural context so all calls will be merged to a single start point. The history is stored as a (shared) list of decisions, effectively a tree
Definition at line 23 of file local_control_flow_history.h.
Member Typedef Documentation
◆ lcfd_ptrt
| typedef std::shared_ptr<const local_control_flow_decisiont> local_control_flow_decisiont::lcfd_ptrt |
Definition at line 29 of file local_control_flow_history.h.
◆ locationt
Definition at line 26 of file local_control_flow_history.h.
Constructor & Destructor Documentation
◆ local_control_flow_decisiont()
|
inline |
Definition at line 32 of file local_control_flow_history.h.
Member Function Documentation
◆ operator<()
| bool local_control_flow_decisiont::operator< | ( | const local_control_flow_decisiont & | op | ) | const |
Definition at line 271 of file local_control_flow_history.cpp.
◆ operator==()
| bool local_control_flow_decisiont::operator== | ( | const local_control_flow_decisiont & | op | ) | const |
Definition at line 331 of file local_control_flow_history.cpp.
Member Data Documentation
◆ branch_location
| locationt local_control_flow_decisiont::branch_location |
Definition at line 27 of file local_control_flow_history.h.
◆ branch_taken
| bool local_control_flow_decisiont::branch_taken |
Definition at line 28 of file local_control_flow_history.h.
◆ previous
| lcfd_ptrt local_control_flow_decisiont::previous |
Definition at line 30 of file local_control_flow_history.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/analyses/local_control_flow_history.h
- /home/runner/work/cbmc/cbmc/src/analyses/local_control_flow_history.cpp
