15 #ifndef CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 16 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 101 "node_id must not be valid");
112 "node_id must be valid");
125 node_id != std::numeric_limits<node_indext>::max(),
126 "node_id must not be valid");
139 "node_id must be valid");
145 "If the domain is top, it must have no dependencies");
153 "node_id must be valid");
159 "If the domain is bottom, it must have no dependencies");
171 assert(
node_id!=std::numeric_limits<node_indext>::max());
183 typedef std::set<goto_programt::const_targett>
depst;
216 public ait<dep_graph_domaint>,
234 rd(goto_functions,
ns);
251 for(
const auto &location_state :
state_map)
253 location_state.second.populate_dep_graph(*
this, location_state.first);
274 std::pair<state_mapt::iterator, bool> entry=
280 entry.first->second.set_node_id(node_id);
284 return entry.first->second;
294 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
void transform(goto_programt::const_targett from, 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...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
A generic directed graph with a parametric node type.
std::set< goto_programt::const_targett > depst
post_dominators_mapt post_dominators
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)
void make_entry() final override
a reasonable entry-point state
grapht< dep_nodet >::node_indext node_indext
bool is_top() const final override
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
void set_node_id(node_indext id)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
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
instructionst::const_iterator const_targett
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
const post_dominators_mapt & cfg_post_dominators() const
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
nodet::node_indext node_indext
depst control_dep_candidates
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
goto_programt::const_targett PC
A generic container class for the GOTO intermediate representation of one function.
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
friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &)
dependence_grapht(const namespacet &_ns)
The basic interface of an abstract interpreter.
bool merge(const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
graph_nodet< dep_edget >::edgest edgest
void make_bottom() final override
no states
bool empty() const
Is the program empty?
virtual void initialize(const goto_programt &)
static const irep_idt get_function_id(const_targett l)
goto_programt & goto_program
node_indext get_node_id() const
bool is_bottom() const final override
#define DATA_INVARIANT(CONDITION, REASON)
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.
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)