CBMC
|
This ensures that all domains are constructed with the node ID that links them to the graph part of the dependency graph. More...
Public Member Functions | |
dep_graph_domain_factoryt (dependence_grapht &_dg, message_handlert &message_handler) | |
std::unique_ptr< statet > | make (locationt l) const override |
Public Member Functions inherited from ai_domain_factoryt< dep_graph_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 | |
dependence_grapht & | dg |
message_handlert & | message_handler |
Additional Inherited Members | |
Public Types inherited from ai_domain_factoryt< dep_graph_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 |
This ensures that all domains are constructed with the node ID that links them to the graph part of the dependency graph.
Using a factory is a tad verbose but it works well with the ait infrastructure.
Definition at line 341 of file dependence_graph.cpp.
|
inline |
Definition at line 344 of file dependence_graph.cpp.
Implements ai_domain_factory_baset.
Definition at line 351 of file dependence_graph.cpp.
|
private |
Definition at line 362 of file dependence_graph.cpp.
|
private |
Definition at line 363 of file dependence_graph.cpp.