CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Types | Protected Attributes | List of all members
sparse_bitvector_analysist< V > Class Template Reference

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 >:
[フレーム]
[legend]
+ Collaboration diagram for sparse_bitvector_analysist< V >:
[フレーム]
[legend]

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.
 
std::unordered_map< irep_idt, inner_mapt >  value_map
  A map from names of program variables to a set of pairs (reaching_definitiont , ID).
 

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

template<typename V >
typedef std::map<V, std::size_t> sparse_bitvector_analysist< V >::inner_mapt
protected

Definition at line 71 of file reaching_definitions.h.

Member Function Documentation

◆  add()

template<typename V >
std::size_t sparse_bitvector_analysist< V >::add ( const V &  value )
inline

Definition at line 51 of file reaching_definitions.h.

◆  clear()

template<typename V >
void sparse_bitvector_analysist< V >::clear ( )
inline

Definition at line 64 of file reaching_definitions.h.

◆  get()

template<typename V >
const V & sparse_bitvector_analysist< V >::get ( const std::size_t  value_index ) const
inline

Definition at line 45 of file reaching_definitions.h.

Member Data Documentation

◆  value_map

template<typename V >
std::unordered_map<irep_idt, inner_mapt> sparse_bitvector_analysist< V >::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

template<typename V >
std::vector<typename inner_mapt::const_iterator> sparse_bitvector_analysist< V >::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:

AltStyle によって変換されたページ (->オリジナル) /