CBMC
invariant_set_domain_factoryt Class Reference

Pass the necessary arguments to the invariant_set_domaint's when constructed. More...

+ Inheritance diagram for invariant_set_domain_factoryt:
+ Collaboration diagram for invariant_set_domain_factoryt:

Public Member Functions

 invariant_set_domain_factoryt (invariant_propagationt &_ip)
 
std::unique_ptr< statetmake (locationt l) const override
 
- Public Member Functions inherited from ai_domain_factoryt< invariant_set_domaint >
std::unique_ptr< statetcopy (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

invariant_propagationtip
 

Additional Inherited Members

- Public Types inherited from ai_domain_factoryt< invariant_set_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

Pass the necessary arguments to the invariant_set_domaint's when constructed.

Definition at line 18 of file invariant_propagation.cpp.

Constructor & Destructor Documentation

◆ invariant_set_domain_factoryt()

invariant_set_domain_factoryt::invariant_set_domain_factoryt ( invariant_propagationt _ip)
inlineexplicit

Definition at line 22 of file invariant_propagation.cpp.

Member Function Documentation

◆ make()

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

Implements ai_domain_factory_baset.

Definition at line 26 of file invariant_propagation.cpp.

Member Data Documentation

◆ ip

invariant_propagationt& invariant_set_domain_factoryt::ip
private

Definition at line 36 of file invariant_propagation.cpp.


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