cprover
|
#include <dependence_graph.h>
Public Types | |
typedef grapht< dep_nodet >::node_indext | node_indext |
![]() | |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
dep_graph_domaint () | |
bool | merge (const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to) |
void | transform (goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) final |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final |
jsont | output_json (const ai_baset &ai, const namespacet &ns) const override |
Outputs the current value of the domain. More... | |
void | make_top () final override |
void | make_bottom () final |
void | make_entry () final |
void | set_node_id (node_indext id) |
node_indext | get_node_id () const |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
virtual bool | ai_simplify (exprt &condition, const namespacet &ns) const |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Use the information in the domain to simplify the expression on the LHS of an assignment. More... | |
Private Types | |
typedef std::set< goto_programt::const_targett > | depst |
Private Member Functions | |
void | control_dependencies (goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph) |
void | data_dependencies (goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns) |
Private Attributes | |
tvt | has_values |
node_indext | node_id |
depst | control_deps |
depst | data_deps |
Definition at line 66 of file dependence_graph.h.
|
private |
Definition at line 135 of file dependence_graph.h.
Definition at line 69 of file dependence_graph.h.
|
inline |
Definition at line 71 of file dependence_graph.h.
|
private |
Definition at line 63 of file dependence_graph.cpp.
References dependence_grapht::add_dep(), cfg_dominators_templatet< P, T, post_dom >::cfg, dependence_grapht::cfg_post_dominators(), control_deps, dep_edget::CTRL, cfg_dominators_templatet< P, T, post_dom >::nodet::dominators, cfg_baset< T, P, I >::entry_map, and goto_program_templatet< codet, exprt >::get_function_id().
Referenced by transform().
|
private |
Definition at line 150 of file dependence_graph.cpp.
References dependence_grapht::add_dep(), dep_edget::DATA, data_deps, forall_rw_range_set_r_objects, sparse_bitvector_analysist< V >::get(), rw_range_sett::get_ranges(), dependence_grapht::get_state(), reaching_definitions_analysist::get_value_sets(), goto_rw(), may_be_def_use_pair(), and dependence_grapht::reaching_definitions().
Referenced by transform().
|
inline |
Definition at line 125 of file dependence_graph.h.
References node_id.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 106 of file dependence_graph.h.
References control_deps, data_deps, has_values, and node_id.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 115 of file dependence_graph.h.
References make_top().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 97 of file dependence_graph.h.
References control_deps, data_deps, has_values, and node_id.
Referenced by make_entry().
bool dep_graph_domaint::merge | ( | const dep_graph_domaint & | src, |
goto_programt::const_targett | from, | ||
goto_programt::const_targett | to | ||
) |
Definition at line 24 of file dependence_graph.cpp.
References control_deps, data_deps, has_values, tvt::is_false(), and tvt::unknown().
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 246 of file dependence_graph.cpp.
References control_deps, and data_deps.
|
overridevirtual |
Outputs the current value of the domain.
Reimplemented from ai_domain_baset.
Definition at line 285 of file dependence_graph.cpp.
References control_deps, data_deps, json(), jsont::make_object(), and json_arrayt::push_back().
|
inline |
Definition at line 120 of file dependence_graph.h.
References node_id.
|
final |
Definition at line 199 of file dependence_graph.cpp.
References control_dependencies(), control_deps, data_dependencies(), and dependence_grapht::get_state().
|
private |
Definition at line 136 of file dependence_graph.h.
Referenced by control_dependencies(), make_bottom(), make_top(), merge(), output(), output_json(), and transform().
|
private |
Definition at line 136 of file dependence_graph.h.
Referenced by data_dependencies(), make_bottom(), make_top(), merge(), output(), and output_json().
|
private |
Definition at line 132 of file dependence_graph.h.
Referenced by make_bottom(), make_top(), and merge().
|
private |
Definition at line 133 of file dependence_graph.h.
Referenced by get_node_id(), make_bottom(), make_top(), and set_node_id().