CBMC
|
Pass the necessary arguments to the invariant_set_domaint's when constructed. More...
Public Member Functions | |
invariant_set_domain_factoryt (invariant_propagationt &_ip) | |
std::unique_ptr< statet > | make (locationt l) const override |
Public Member Functions inherited from ai_domain_factoryt< invariant_set_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 | |
invariant_propagationt & | ip |
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 |
Pass the necessary arguments to the invariant_set_domaint's when constructed.
Definition at line 18 of file invariant_propagation.cpp.
|
inlineexplicit |
Definition at line 22 of file invariant_propagation.cpp.
|
inlineoverridevirtual |
Implements ai_domain_factory_baset.
Definition at line 26 of file invariant_propagation.cpp.
|
private |
Definition at line 36 of file invariant_propagation.cpp.