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");
166 assert(
node_id!=std::numeric_limits<node_indext>::max());
178 typedef std::set<goto_programt::const_targett>
depst;
215 public ait<dep_graph_domaint>,
229 rd(goto_functions,
ns);
240 if(!goto_program.
empty())
249 for(
const auto &location_state :
252 std::static_pointer_cast<dep_graph_domaint>(location_state.second)
253 ->populate_dep_graph(*
this, location_state.first);
Compute dominators for CFG of goto_function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
virtual void make_bottom()=0
no states
ai_history_baset::trace_ptrt trace_ptrt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
bool is_top() const final override
friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &)
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
node_indext get_node_id() const
bool is_bottom() const final override
void make_bottom() final override
no states
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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...
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)
depst control_dep_candidates
bool merge(const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
dep_graph_domaint(node_indext id)
void data_dependencies(goto_programt::const_targett from, const irep_idt &function_to, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
std::set< goto_programt::const_targett > depst
void make_entry() final override
Make this domain a reasonable entry-point state.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
grapht< dep_nodet >::node_indext node_indext
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
friend dep_graph_domain_factoryt
const reaching_definitions_analysist & reaching_definitions() const
const post_dominators_mapt & cfg_post_dominators() const
reaching_definitions_analysist rd
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
void initialize(const goto_functionst &goto_functions)
Initialize all the abstract states for a whole program.
dependence_grapht(const namespacet &_ns)
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
void initialize(const irep_idt &function, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
post_dominators_mapt post_dominators
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
bool empty() const
Is the program empty?
This class represents a node in a directed graph.
A generic directed graph with a parametric node type.
The most conventional storage; one domain per location.
state_mapt & internal(void)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
graph_nodet< dep_edget >::edget edget
graph_nodet< dep_edget >::edgest edgest
goto_programt::const_targett PC