73 if(from->is_goto() || from->is_assume())
75 else if(from->is_end_function())
95 bool post_dom_all = !control_dep_candidate->is_assume();
96 bool post_dom_one=
false;
100 cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e =
104 e != pd.
cfg.
entry_map.end(),
"cfg must have an entry for every location");
110 for(
const auto &edge : m.out)
121 if(post_dom_all || !post_dom_one)
141 if((w_end!=-1 && w_end <= r_start) ||
142 (r_end!=-1 && w_start >= r_end))
144 else if(w_start >= r_start)
147 (r_end!=-1 && w_end > r_start))
174 for(
const auto &w_range : w_ranges)
177 for(
const auto &wr : w_range.second)
178 for(
const auto &r_range : r_ranges)
181 r_range.first, r_range.second))
200 assert(dep_graph!=
nullptr);
203 if(from->is_function_call())
205 if(from->function == to->function)
245 out <<
"Control dependencies: ";
246 for(depst::const_iterator
253 out << (*it)->location_number;
260 out <<
"Data dependencies: ";
261 for(depst::const_iterator
268 out << (*it)->location_number;
286 link[
"locationNumber"]=
288 link[
"sourceLocation"]=
json(cd->source_location);
295 link[
"locationNumber"]=
297 link[
"sourceLocation"]=
json(dd->source_location);
311 assert(n_from<
size());
318 nodes[n_from].out[n_to].add(kind);
319 nodes[n_to].in[n_from].add(kind);
void transform(goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) final override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
const reaching_definitions_analysist & reaching_definitions() const
#define INVARIANT(CONDITION, REASON)
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
jsont & push_back(const jsont &json)
void control_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
instructionst::const_iterator const_targett
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
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
value_setst & get_value_sets() const
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
nodet::node_indext node_indext
depst control_dep_candidates
#define forall_rw_range_set_r_objects(it, rw_set)
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
const V & get(const std::size_t value_index) const
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)
bool merge(const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool is_bottom() const final override
const range_domaint & get_ranges(objectst::const_iterator it) const
json_objectt & make_object()
virtual statet & get_state(goto_programt::const_targett l)
std::map< locationt, rangest > ranges_at_loct
json_objectt json(const source_locationt &location)