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
 

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 (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
 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...
 
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
 
void set_node_id (node_indext id)
 
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 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'. More...
 

Detailed Description

Definition at line 66 of file dependence_graph.h.

Member Typedef Documentation

◆ depst

Definition at line 185 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()

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

◆ get_node_id()

node_indext dep_graph_domaint::get_node_id ( ) const
inline

Definition at line 171 of file dependence_graph.h.

◆ is_bottom()

bool dep_graph_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 152 of file dependence_graph.h.

◆ is_top()

bool dep_graph_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 138 of file dependence_graph.h.

◆ make_bottom()

void dep_graph_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 111 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 124 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 100 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 245 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 284 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 328 of file dependence_graph.cpp.

◆ set_node_id()

void dep_graph_domaint::set_node_id ( node_indext  id)
inline

Definition at line 166 of file dependence_graph.h.

◆ 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

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)

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

Implements ai_domain_baset.

Definition at line 198 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 194 of file dependence_graph.h.

◆ control_deps

depst dep_graph_domaint::control_deps
private

Definition at line 189 of file dependence_graph.h.

◆ data_deps

depst dep_graph_domaint::data_deps
private

Definition at line 198 of file dependence_graph.h.

◆ has_changed

bool dep_graph_domaint::has_changed
private

Definition at line 183 of file dependence_graph.h.

◆ has_values

tvt dep_graph_domaint::has_values
private

Definition at line 181 of file dependence_graph.h.

◆ node_id

node_indext dep_graph_domaint::node_id
private

Definition at line 182 of file dependence_graph.h.


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