cprover
dep_graph_domaint Class Reference

#include <dependence_graph.h>

+ Inheritance diagram for dep_graph_domaint:
+ Collaboration diagram for dep_graph_domaint:

Public Types

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

Public Member Functions

 dep_graph_domaint (node_indext id)
 
bool merge (const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
 
void transform (const irep_idt &function_from, goto_programt::const_targett from, const irep_idt &function_to, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) final override
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
 
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
 all states – the analysis doesn't use this, and domains may refuse to implement it. More...
 
void make_bottom () final override
 no states More...
 
void make_entry () final override
 Make this domain a reasonable entry-point state. More...
 
bool is_top () const final override
 
bool is_bottom () const final override
 
node_indext get_node_id () const
 
void populate_dep_graph (dependence_grapht &, goto_programt::const_targett) const
 
- Public Member Functions inherited from ai_domain_baset
virtual ~ai_domain_baset ()
 
virtual void transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns)
 how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More...
 
virtual xmlt output_xml (const ai_baset &ai, const namespacet &ns) const
 
virtual bool ai_simplify (exprt &condition, const namespacet &) const
 also add More...
 
virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Simplifies the expression but keeps it as an l-value. More...
 
virtual exprt to_predicate (void) const
 Gives a Boolean condition that is true for all values represented by the domain. More...
 

Private Types

typedef std::set< goto_programt::const_targettdepst
 

Private Member Functions

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

Private Attributes

tvt has_values
 
node_indext node_id
 
bool has_changed
 
depst control_deps
 
depst control_dep_candidates
 
depst data_deps
 

Friends

const depstdependence_graph_test_get_control_deps (const dep_graph_domaint &)
 
const depstdependence_graph_test_get_data_deps (const dep_graph_domaint &)
 

Additional Inherited Members

- Protected Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More...
 
 ai_domain_baset (const ai_domain_baset &old)
 A copy constructor is part of the domain interface. More...
 

Detailed Description

Definition at line 66 of file dependence_graph.h.

Member Typedef Documentation

◆ depst

Definition at line 178 of file dependence_graph.h.

◆ node_indext

Constructor & Destructor Documentation

◆ dep_graph_domaint()

dep_graph_domaint::dep_graph_domaint ( node_indext  id)
inlineexplicit

Definition at line 71 of file dependence_graph.h.

Member Function Documentation

◆ control_dependencies()

void dep_graph_domaint::control_dependencies ( const irep_idt function_id,
goto_programt::const_targett  from,
goto_programt::const_targett  to,
dependence_grapht dep_graph 
)
private

Definition at line 54 of file dependence_graph.cpp.

◆ data_dependencies()

void dep_graph_domaint::data_dependencies ( goto_programt::const_targett  from,
const irep_idt function_to,
goto_programt::const_targett  to,
dependence_grapht dep_graph,
const namespacet ns 
)
private

Definition at line 150 of file dependence_graph.cpp.

◆ get_node_id()

node_indext dep_graph_domaint::get_node_id ( ) const
inline

Definition at line 164 of file dependence_graph.h.

◆ is_bottom()

bool dep_graph_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 150 of file dependence_graph.h.

◆ is_top()

bool dep_graph_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 136 of file dependence_graph.h.

◆ make_bottom()

void dep_graph_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 109 of file dependence_graph.h.

◆ make_entry()

void dep_graph_domaint::make_entry ( )
inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 122 of file dependence_graph.h.

◆ make_top()

void dep_graph_domaint::make_top ( )
inlinefinaloverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 98 of file dependence_graph.h.

◆ 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.

◆ output()

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

Reimplemented from ai_domain_baset.

Definition at line 264 of file dependence_graph.cpp.

◆ 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 303 of file dependence_graph.cpp.

◆ populate_dep_graph()

void dep_graph_domaint::populate_dep_graph ( dependence_grapht dep_graph,
goto_programt::const_targett  this_loc 
) const

Definition at line 378 of file dependence_graph.cpp.

◆ transform()

void dep_graph_domaint::transform ( const irep_idt function_from,
goto_programt::const_targett  from,
const irep_idt function_to,
goto_programt::const_targett  to,
ai_baset ai,
const namespacet ns 
)
finaloverridevirtual
Deprecated:
SINCE(2019, 08, 01, "use the history signature instead")

Implements ai_domain_baset.

Definition at line 195 of file dependence_graph.cpp.

Friends And Related Function Documentation

◆ dependence_graph_test_get_control_deps

const depst& dependence_graph_test_get_control_deps ( const dep_graph_domaint )
friend

◆ dependence_graph_test_get_data_deps

const depst& dependence_graph_test_get_data_deps ( const dep_graph_domaint )
friend

Member Data Documentation

◆ control_dep_candidates

depst dep_graph_domaint::control_dep_candidates
private

Definition at line 187 of file dependence_graph.h.

◆ control_deps

depst dep_graph_domaint::control_deps
private

Definition at line 182 of file dependence_graph.h.

◆ data_deps

depst dep_graph_domaint::data_deps
private

Definition at line 191 of file dependence_graph.h.

◆ has_changed

bool dep_graph_domaint::has_changed
private

Definition at line 176 of file dependence_graph.h.

◆ has_values

tvt dep_graph_domaint::has_values
private

Definition at line 174 of file dependence_graph.h.

◆ node_id

node_indext dep_graph_domaint::node_id
private

Definition at line 175 of file dependence_graph.h.


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