15 #ifndef CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 16 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 99 assert(
node_id!=std::numeric_limits<node_indext>::max());
108 assert(
node_id!=std::numeric_limits<node_indext>::max());
127 assert(
node_id!=std::numeric_limits<node_indext>::max());
135 typedef std::set<goto_programt::const_targett>
depst;
151 public ait<dep_graph_domaint>,
169 rd(goto_functions,
ns);
176 if(!goto_program.
empty())
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)
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
grapht< dep_nodet >::node_indext node_indext
instructionst::const_iterator const_targett
void set_node_id(node_indext id)
void make_top() final override
void control_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
void transform(goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) final
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...
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
A Template Class for Graphs.
graph_nodet< dep_edget >::edget edget
dependence_grapht(const namespacet &_ns)
bool merge(const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
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.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final