CBMC
Public Member Functions | Private Attributes | List of all members
rd_range_domain_factoryt Class Reference

This ensures that all domains are constructed with the appropriate pointer back to the analysis engine itself. More...

+ Inheritance diagram for rd_range_domain_factoryt:
+ Collaboration diagram for rd_range_domain_factoryt:

Public Member Functions

 rd_range_domain_factoryt (sparse_bitvector_analysist< reaching_definitiont > *_bv_container, message_handlert &message_handler)
 
std::unique_ptr< statet > make (locationt) const override
 
- Public Member Functions inherited from ai_domain_factoryt< rd_range_domaint >
std::unique_ptr< statet > copy (const statet &s) const override
 
bool merge (statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const override
 
- Public Member Functions inherited from ai_domain_factory_baset
virtual ~ai_domain_factory_baset ()
 

Private Attributes

sparse_bitvector_analysist< reaching_definitiont > *const bv_container
 
message_handlert & message_handler
 

Additional Inherited Members

- Public Types inherited from ai_domain_factoryt< rd_range_domaint >
typedef ai_domain_factory_baset::statet statet
 
typedef ai_domain_factory_baset::locationt locationt
 
typedef ai_domain_factory_baset::trace_ptrt trace_ptrt
 
- Public Types inherited from ai_domain_factory_baset
typedef ai_domain_baset statet
 
typedef ai_domain_baset::locationt locationt
 
typedef ai_domain_baset::trace_ptrt trace_ptrt
 

Detailed Description

This ensures that all domains are constructed with the appropriate pointer back to the analysis engine itself.

Using a factory is a tad verbose but it works well with the ait infrastructure.

Definition at line 31 of file reaching_definitions.cpp.

Constructor & Destructor Documentation

◆ rd_range_domain_factoryt()

rd_range_domain_factoryt::rd_range_domain_factoryt ( sparse_bitvector_analysist< reaching_definitiont > *  _bv_container,
message_handlert &  message_handler 
)
inline

Definition at line 34 of file reaching_definitions.cpp.

Member Function Documentation

◆ make()

std::unique_ptr<statet> rd_range_domain_factoryt::make ( locationt  ) const
inlineoverridevirtual

Implements ai_domain_factory_baset.

Definition at line 42 of file reaching_definitions.cpp.

Member Data Documentation

◆ bv_container

sparse_bitvector_analysist<reaching_definitiont>* const rd_range_domain_factoryt::bv_container
private

Definition at line 50 of file reaching_definitions.cpp.

◆ message_handler

message_handlert& rd_range_domain_factoryt::message_handler
private

Definition at line 51 of file reaching_definitions.cpp.

The documentation for this class was generated from the following file: