cprover
dependence_grapht Class Reference

#include <dependence_graph.h>

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

Public Types

typedef std::map< irep_idt, cfg_post_dominatorstpost_dominators_mapt
 
- Public Types inherited from ait< dep_graph_domaint >
typedef goto_programt::const_targett locationt
 
- Public Types inherited from ai_baset
typedef ai_domain_baset statet
 
typedef goto_programt::const_targett locationt
 
- Public Types inherited from grapht< dep_nodet >
typedef dep_nodet nodet
 
typedef nodet::edgest edgest
 
typedef std::vector< nodetnodest
 
typedef nodet::edget edget
 
typedef nodet::node_indext node_indext
 
typedef std::list< node_indextpatht
 

Public Member Functions

 dependence_grapht (const namespacet &_ns)
 
void initialize (const goto_functionst &goto_functions)
 
void initialize (const goto_programt &goto_program)
 
void add_dep (dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
 
const post_dominators_maptcfg_post_dominators () const
 
const reaching_definitions_analysistreaching_definitions () const
 
virtual statetget_state (goto_programt::const_targett l)
 
- Public Member Functions inherited from ait< dep_graph_domaint >
 ait ()
 
dep_graph_domaintoperator[] (locationt l)
 
const dep_graph_domaintoperator[] (locationt l) const
 
void clear () override
 
- Public Member Functions inherited from ai_baset
 ai_baset ()
 
virtual ~ai_baset ()
 
void operator() (const goto_programt &goto_program, const namespacet &ns)
 
void operator() (const goto_functionst &goto_functions, const namespacet &ns)
 
void operator() (const goto_modelt &goto_model)
 
void operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 
virtual void output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
 
void output (const goto_modelt &goto_model, std::ostream &out) const
 
void output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
 
void output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
 
virtual jsont output_json (const namespacet &ns, const goto_functionst &goto_functions) const
 Output the domains for the whole program as JSON. More...
 
jsont output_json (const goto_modelt &goto_model) const
 
jsont output_json (const namespacet &ns, const goto_programt &goto_program) const
 
jsont output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
 
virtual xmlt output_xml (const namespacet &ns, const goto_functionst &goto_functions) const
 Output the domains for the whole program as XML. More...
 
xmlt output_xml (const goto_modelt &goto_model) const
 
xmlt output_xml (const namespacet &ns, const goto_programt &goto_program) const
 
xmlt output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
 
- Public Member Functions inherited from grapht< dep_nodet >
node_indext add_node ()
 
void swap (grapht &other)
 
bool has_edge (node_indext i, node_indext j) const
 
const nodetoperator[] (node_indext n) const
 
nodetoperator[] (node_indext n)
 
void resize (node_indext s)
 
std::size_t size () const
 
bool empty () const
 
const edgestin (node_indext n) const
 
const edgestout (node_indext n) const
 
void add_edge (node_indext a, node_indext b)
 
void remove_edge (node_indext a, node_indext b)
 
edgetedge (node_indext a, node_indext b)
 
void add_undirected_edge (node_indext a, node_indext b)
 
void remove_undirected_edge (node_indext a, node_indext b)
 
void remove_in_edges (node_indext n)
 
void remove_out_edges (node_indext n)
 
void remove_edges (node_indext n)
 
void clear ()
 
void shortest_path (node_indext src, node_indext dest, patht &path) const
 
void shortest_loop (node_indext node, patht &path) const
 
void visit_reachable (node_indext src)
 
void make_chordal ()
 
std::size_t connected_subgraphs (std::vector< node_indext > &subgraph_nr)
 
std::size_t SCCs (std::vector< node_indext > &subgraph_nr)
 
bool is_dag () const
 
std::list< node_indexttopsort () const
 Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph. More...
 
void output_dot (std::ostream &out) const
 
void output_dot_node (std::ostream &out, node_indext n) const
 

Protected Attributes

const namespacetns
 
post_dominators_mapt post_dominators
 
reaching_definitions_analysist rd
 
- Protected Attributes inherited from ait< dep_graph_domaint >
state_mapt state_map
 
- Protected Attributes inherited from ai_baset
recursion_sett recursion_set
 
- Protected Attributes inherited from grapht< dep_nodet >
nodest nodes
 

Additional Inherited Members

- Protected Types inherited from ait< dep_graph_domaint >
typedef std::unordered_map< locationt, dep_graph_domaint, const_target_hashstate_mapt
 
- Protected Types inherited from ai_baset
typedef std::map< unsigned, locationtworking_sett
 
typedef std::set< irep_idtrecursion_sett
 
- Protected Member Functions inherited from ait< dep_graph_domaint >
const statetfind_state (locationt l) const override
 
bool merge (const statet &src, locationt from, locationt to) override
 
statetmake_temporary_state (const statet &s) override
 
void fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override
 
- Protected Member Functions inherited from ai_baset
virtual void initialize (const goto_functionst::goto_functiont &)
 
void entry_state (const goto_programt &)
 
void entry_state (const goto_functionst &)
 
virtual void output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
 
virtual jsont output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
 Output the domains for a single function as JSON. More...
 
virtual xmlt output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const
 Output the domains for a single function as XML. More...
 
locationt get_next (working_sett &working_set)
 
void put_in_working_set (working_sett &working_set, locationt l)
 
bool fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
void sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)
 
void concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns)
 
bool visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
 
bool do_function_call_rec (locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
 
bool do_function_call (locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns)
 
- Protected Member Functions inherited from grapht< dep_nodet >
void shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const
 
void tarjan (class tarjant &t, node_indext v)
 

Detailed Description

Definition at line 150 of file dependence_graph.h.

Member Typedef Documentation

§ post_dominators_mapt

Constructor & Destructor Documentation

§ dependence_grapht()

dependence_grapht::dependence_grapht ( const namespacet _ns)
inlineexplicit

Definition at line 160 of file dependence_graph.h.

Member Function Documentation

§ add_dep()

§ cfg_post_dominators()

const post_dominators_mapt& dependence_grapht::cfg_post_dominators ( ) const
inline

§ get_state()

virtual statet& dependence_grapht::get_state ( goto_programt::const_targett  l)
inlinevirtual

Reimplemented from ait< dep_graph_domaint >.

Definition at line 199 of file dependence_graph.h.

References add_node().

Referenced by dep_graph_domaint::data_dependencies(), and dep_graph_domaint::transform().

§ initialize() [1/2]

void dependence_grapht::initialize ( const goto_functionst goto_functions)
inlinevirtual

Reimplemented from ai_baset.

Definition at line 166 of file dependence_graph.h.

References ai_baset::initialize().

§ initialize() [2/2]

void dependence_grapht::initialize ( const goto_programt goto_program)
inlinevirtual

§ reaching_definitions()

const reaching_definitions_analysist& dependence_grapht::reaching_definitions ( ) const
inline

Definition at line 194 of file dependence_graph.h.

Referenced by dep_graph_domaint::data_dependencies().

Member Data Documentation

§ ns

const namespacet& dependence_grapht::ns
protected

Definition at line 215 of file dependence_graph.h.

§ post_dominators

post_dominators_mapt dependence_grapht::post_dominators
protected

Definition at line 217 of file dependence_graph.h.

§ rd

reaching_definitions_analysist dependence_grapht::rd
protected

Definition at line 218 of file dependence_graph.h.


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