An instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance.
More...
#include <reaching_definitions.h>
Inheritance diagram for sparse_bitvector_analysist< V >: Collaboration diagram for sparse_bitvector_analysist< V >:Public Member Functions | |
| const V & | get (const std::size_t value_index) const |
| std::size_t | add (const V &value) |
| void | clear () |
Protected Types | |
| typedef std::map< V, std::size_t > | inner_mapt |
Protected Attributes | |
| std::vector< typename inner_mapt::const_iterator > | values |
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map. More... | |
| std::unordered_map< irep_idt, inner_mapt > | value_map |
A map from names of program variables to a set of pairs (reaching_definitiont, ID). More... | |
Detailed Description
template<typename V>
class sparse_bitvector_analysist< V >
An instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance.
Requirement: V has a member "identifier" of type irep_idt
Definition at line 42 of file reaching_definitions.h.
Member Typedef Documentation
◆ inner_mapt
|
protected |
Definition at line 71 of file reaching_definitions.h.
Member Function Documentation
◆ add()
|
inline |
Definition at line 51 of file reaching_definitions.h.
◆ clear()
|
inline |
Definition at line 64 of file reaching_definitions.h.
◆ get()
|
inline |
Definition at line 45 of file reaching_definitions.h.
Member Data Documentation
◆ value_map
|
protected |
A map from names of program variables to a set of pairs (reaching_definitiont, ID).
Formally, the map is defined as value_map: var_names -> (reaching_definitiont -> ID).
Definition at line 80 of file reaching_definitions.h.
◆ values
|
protected |
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map.
Namely, the map is implemented as an std::vector of iterators to elements of the map value_map. An index to this vector is the ID of the related reaching_definitiont instance.
Definition at line 76 of file reaching_definitions.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/analyses/reaching_definitions.h
