71 if(from->is_goto() || from->is_assume())
73 else if(from->is_end_function())
98 const cfg_post_dominatorst::cfgt::nodet &m =
102 for(
const auto &edge : m.out)
107 const cfg_post_dominatorst::cfgt::nodet &
m_s=
110 if(
m_s.dominators.find(to)!=
m_s.dominators.end())
160 dep_graph.reaching_definitions().get_value_sets();
212 if(
dep->is_function_call())
219 return d->is_function_call();
221 "All entries must be function calls");
228 if(from->is_function_call())
272 out <<
"Control dependencies: ";
273 for(depst::const_iterator
280 out << (*it)->location_number;
287 out <<
"Data dependencies: ";
288 for(depst::const_iterator
295 out << (*it)->location_number;
313 {
"locationNumber",
json_numbert(std::to_string(
cd->location_number))},
314 {
"sourceLocation",
json(
cd->source_location())},
322 {
"locationNumber",
json_numbert(std::to_string(
dd->location_number))},
323 {
"sourceLocation",
json(
dd->source_location())},
328 return std::move(graph);
348 return std::unique_ptr<statet>(p.release());
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual void clear()
Reset the abstract state.
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ai_domain_factory_baset::locationt locationt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual statet & get_state(locationt l)
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
dep_graph_domain_factoryt(dependence_grapht &_dg)
std::unique_ptr< statet > make(locationt l) const override
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)
bool is_bottom() const final override
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...
depst control_dep_candidates
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 output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
dependence_grapht(const namespacet &_ns)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
instructionst::const_iterator const_targett
nodet::node_indext node_indext
node_indext add_node(arguments &&... values)
jsont & push_back(const jsont &json)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::map< locationt, rangest > ranges_at_loct
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
static bool may_be_def_use_pair(const mp_integer &w_start, const mp_integer &w_end, const mp_integer &r_start, const mp_integer &r_end)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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)
std::unique_ptr< T > util_make_unique(Ts &&... ts)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
#define CHECK_RETURN(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.