cprover
dep_graph_domaint Class Reference

#include <dependence_graph.h>

Inheritance diagram for dep_graph_domaint:
[legend]
Collaboration diagram for dep_graph_domaint:
[legend]

Public Types

typedef grapht< dep_nodet >::node_indext node_indext
 
- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Public Member Functions

 dep_graph_domaint ()
 
bool merge (const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
 
void transform (goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) final
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
 
jsont output_json (const ai_baset &ai, const namespacet &ns) const override
 Outputs the current value of the domain. More...
 
void make_top () final override
 
void make_bottom () final
 
void make_entry () final
 
void set_node_id (node_indext id)
 
node_indext get_node_id () const
 
- Public Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 
virtual ~ai_domain_baset ()
 
virtual void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
 
virtual xmlt output_xml (const ai_baset &ai, const namespacet &ns) const
 
virtual bool ai_simplify (exprt &condition, const namespacet &ns) const
 
virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Use the information in the domain to simplify the expression on the LHS of an assignment. More...
 

Private Types

typedef std::set< goto_programt::const_targettdepst
 

Private Member Functions

void control_dependencies (goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
 
void data_dependencies (goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
 

Private Attributes

tvt has_values
 
node_indext node_id
 
depst control_deps
 
depst data_deps
 

Detailed Description

Definition at line 66 of file dependence_graph.h.

Member Typedef Documentation

◆ depst

Definition at line 135 of file dependence_graph.h.

◆ node_indext

Constructor & Destructor Documentation

◆ dep_graph_domaint()

dep_graph_domaint::dep_graph_domaint ( )
inline

Definition at line 71 of file dependence_graph.h.

Member Function Documentation

◆ control_dependencies()

◆ data_dependencies()

◆ get_node_id()

node_indext dep_graph_domaint::get_node_id ( ) const
inline

Definition at line 125 of file dependence_graph.h.

References node_id.

◆ make_bottom()

void dep_graph_domaint::make_bottom ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 106 of file dependence_graph.h.

References control_deps, data_deps, has_values, and node_id.

◆ make_entry()

void dep_graph_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 115 of file dependence_graph.h.

References make_top().

◆ make_top()

void dep_graph_domaint::make_top ( )
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 97 of file dependence_graph.h.

References control_deps, data_deps, has_values, and node_id.

Referenced by make_entry().

◆ merge()

bool dep_graph_domaint::merge ( const dep_graph_domaint src,
goto_programt::const_targett  from,
goto_programt::const_targett  to 
)

Definition at line 24 of file dependence_graph.cpp.

References control_deps, data_deps, has_values, tvt::is_false(), and tvt::unknown().

◆ output()

void dep_graph_domaint::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
finalvirtual

Reimplemented from ai_domain_baset.

Definition at line 246 of file dependence_graph.cpp.

References control_deps, and data_deps.

◆ output_json()

jsont dep_graph_domaint::output_json ( const ai_baset ai,
const namespacet ns 
) const
overridevirtual

Outputs the current value of the domain.

parameters: The abstract interpreter and the namespace.
Returns
The domain, formatted as a JSON object.

Reimplemented from ai_domain_baset.

Definition at line 285 of file dependence_graph.cpp.

References control_deps, data_deps, json(), jsont::make_object(), and json_arrayt::push_back().

◆ set_node_id()

void dep_graph_domaint::set_node_id ( node_indext  id)
inline

Definition at line 120 of file dependence_graph.h.

References node_id.

◆ transform()

void dep_graph_domaint::transform ( goto_programt::const_targett  from,
goto_programt::const_targett  to,
ai_baset ai,
const namespacet ns 
)
final

Member Data Documentation

◆ control_deps

depst dep_graph_domaint::control_deps
private

◆ data_deps

depst dep_graph_domaint::data_deps
private

Definition at line 136 of file dependence_graph.h.

Referenced by data_dependencies(), make_bottom(), make_top(), merge(), output(), and output_json().

◆ has_values

tvt dep_graph_domaint::has_values
private

Definition at line 132 of file dependence_graph.h.

Referenced by make_bottom(), make_top(), and merge().

◆ node_id

node_indext dep_graph_domaint::node_id
private

Definition at line 133 of file dependence_graph.h.

Referenced by get_node_id(), make_bottom(), make_top(), and set_node_id().


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