15 #ifndef CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 16 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 73 node_id(
std::numeric_limits<node_indext>::max())
99 assert(node_id!=std::numeric_limits<node_indext>::max());
101 has_values=
tvt(
true);
102 control_deps.clear();
108 assert(node_id!=std::numeric_limits<node_indext>::max());
110 has_values=
tvt(
false);
111 control_deps.clear();
127 assert(node_id!=std::numeric_limits<node_indext>::max());
135 typedef std::set<goto_programt::const_targett>
depst;
138 void control_dependencies(
143 void data_dependencies(
151 public ait<dep_graph_domaint>,
169 rd(goto_functions, ns);
176 if(!goto_program.
empty())
191 return post_dominators;
201 std::pair<state_mapt::iterator, bool> entry=
207 entry.first->second.set_node_id(node_id);
211 return entry.first->second;
221 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
A generic directed graph with a parametric node type.
std::set< goto_programt::const_targett > depst
post_dominators_mapt post_dominators
static const irep_idt get_function_id(const_targett l)
bool empty() const
Is the program empty?
void initialize(const goto_programt &goto_program)
reaching_definitions_analysist rd
const reaching_definitions_analysist & reaching_definitions() const
void initialize(const goto_functionst &goto_functions)
grapht< dep_nodet >::node_indext node_indext
instructionst::const_iterator const_targett
void set_node_id(node_indext id)
void make_top() final override
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
static graphmlt::node_indext add_node(const std::string &name, name_mapt &name_to_node, graphmlt &graph)
const post_dominators_mapt & cfg_post_dominators() const
nodet::node_indext node_indext
goto_programt::const_targett PC
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
A Template Class for Graphs.
graph_nodet< dep_edget >::edget edget
dependence_grapht(const namespacet &_ns)
graph_nodet< dep_edget >::edgest edgest
virtual void initialize(const goto_programt &)
node_indext get_node_id() const
Compute dominators for CFG of goto_function.
virtual statet & get_state(goto_programt::const_targett l)
This class represents a node in a directed graph.