Go to the documentation of this file.
71 if(from->is_goto() || from->is_assume())
73 else if(from->is_end_function())
93 bool post_dom_all = !control_dep_candidate->is_assume();
94 bool post_dom_one=
false;
102 for(
const auto &edge : m.out)
116 if(post_dom_all || !post_dom_one)
142 else if(w_start >= r_start)
168 goto_rw(function_to, to, rw_set);
170 for(
const auto &read_object_entry : rw_set.
get_r_set())
176 for(
const auto &w_range : w_ranges)
179 for(
const auto &wr : w_range.second)
181 for(
const auto &r_range : r_ranges)
185 r_range.first, r_range.second))
198 if(to->is_set_return_value())
225 locationt from{trace_from->current_location()};
226 locationt to{trace_to->current_location()};
229 assert(dep_graph!=
nullptr);
233 depst filtered_control_deps;
237 std::inserter(filtered_control_deps, filtered_control_deps.end()),
242 if(from->is_function_call() && function_from != function_to)
279 out <<
"Control dependencies: ";
280 for(depst::const_iterator
287 out << (*it)->location_number;
294 out <<
"Data dependencies: ";
295 for(depst::const_iterator
302 out << (*it)->location_number;
321 {
"sourceLocation",
json(cd->source_location())},
330 {
"sourceLocation",
json(dd->source_location())},
335 return std::move(graph);
352 auto p = util_make_unique<dep_graph_domaint>(node_id);
355 return std::unique_ptr<statet>(p.release());
374 const node_indext n_from = (*this)[from].get_node_id();
375 assert(n_from<
size());
376 const node_indext n_to = (*this)[to].get_node_id();
382 nodes[n_from].out[n_to].add(kind);
383 nodes[n_to].in[n_from].add(kind);
const reaching_definitions_analysist & reaching_definitions() const
std::map< irep_idt, goto_programt::const_targett > end_function_map
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const objectst & get_r_set() const
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...
static bool may_be_def_use_pair(const range_spect &w_start, const range_spect &w_end, const range_spect &r_start, const range_spect &r_end)
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
dependence_grapht(const namespacet &_ns)
#define CHECK_RETURN(CONDITION)
value_setst & get_value_sets() const
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
const post_dominators_mapt & cfg_post_dominators() const
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
node_indext add_node(arguments &&... values)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::map< locationt, rangest > ranges_at_loct
bool is_bottom() const final override
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
ai_history_baset::trace_ptrt trace_ptrt
nodet::node_indext node_indext
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
dep_graph_domain_factoryt(dependence_grapht &_dg)
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
std::unique_ptr< statet > make(locationt l) const override
#define PRECONDITION(CONDITION)
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
std::set< goto_programt::const_targett > depst
depst control_dep_candidates
goto_programt::const_targett locationt
bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)
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)
This is the basic interface of the abstract interpreter with default implementations of the core func...
ai_domain_baset::locationt locationt
instructionst::const_iterator const_targett
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
virtual statet & get_state(locationt l)
const V & get(const std::size_t value_index) const
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
jsont & push_back(const jsont &json)