15 #ifndef CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 16 #define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H 103 "node_id must not be valid");
114 "node_id must be valid");
127 node_id != std::numeric_limits<node_indext>::max(),
128 "node_id must not be valid");
141 "node_id must be valid");
147 "If the domain is top, it must have no dependencies");
155 "node_id must be valid");
161 "If the domain is bottom, it must have no dependencies");
173 assert(
node_id!=std::numeric_limits<node_indext>::max());
185 typedef std::set<goto_programt::const_targett>
depst;
218 public ait<dep_graph_domaint>,
236 rd(goto_functions,
ns);
243 if(!goto_program.
empty())
253 for(
const auto &location_state :
state_map)
255 location_state.second.populate_dep_graph(*
this, location_state.first);
276 std::pair<state_mapt::iterator, bool> entry=
282 entry.first->second.set_node_id(node_id);
286 return entry.first->second;
296 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
A generic directed graph with a parametric node type.
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...
std::set< goto_programt::const_targett > depst
post_dominators_mapt post_dominators
void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
reaching_definitions_analysist rd
const reaching_definitions_analysist & reaching_definitions() const
void initialize(const goto_functionst &goto_functions)
Initialize all the abstract states for a whole program.
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
void make_entry() final override
Make this domain 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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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
A collection of goto functions.
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?
static const irep_idt get_function_id(const_targett l)
Get the id of the function that contains the instruction pointed-to by the given instruction iterator...
node_indext get_node_id() const
bool is_bottom() const final override
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Compute dominators for CFG of goto_function.
virtual statet & get_state(goto_programt::const_targett l)
Get the state for the given location, creating it in a default way if it doesn't exist.
This class represents a node in a directed graph.
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)