cprover
|
#include <dependence_graph.h>
Public Types | |
typedef grapht< dep_nodet >::node_indext | node_indext |
![]() | |
typedef goto_programt::const_targett | locationt |
typedef ai_history_baset::trace_ptrt | trace_ptrt |
Public Member Functions | |
dep_graph_domaint (node_indext id) | |
bool | merge (const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to) |
void | transform (const irep_idt &function_from, goto_programt::const_targett from, const irep_idt &function_to, 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 |
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 |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
void | make_bottom () final override |
no states More... | |
void | make_entry () final override |
Make this domain a reasonable entry-point state. More... | |
bool | is_top () const final override |
bool | is_bottom () const final override |
node_indext | get_node_id () const |
void | populate_dep_graph (dependence_grapht &, goto_programt::const_targett) const |
![]() | |
virtual | ~ai_domain_baset () |
virtual void | transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns) |
how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More... | |
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
virtual bool | ai_simplify (exprt &condition, const namespacet &) const |
also add More... | |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Simplifies the expression but keeps it as an l-value. More... | |
virtual exprt | to_predicate (void) const |
Gives a Boolean condition that is true for all values represented by the domain. More... | |
Private Types | |
typedef std::set< goto_programt::const_targett > | depst |
Private Member Functions | |
void | control_dependencies (const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph) |
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) |
Private Attributes | |
tvt | has_values |
node_indext | node_id |
bool | has_changed |
depst | control_deps |
depst | control_dep_candidates |
depst | data_deps |
Friends | |
const depst & | dependence_graph_test_get_control_deps (const dep_graph_domaint &) |
const depst & | dependence_graph_test_get_data_deps (const dep_graph_domaint &) |
Additional Inherited Members | |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More... | |
ai_domain_baset (const ai_domain_baset &old) | |
A copy constructor is part of the domain interface. More... | |
Definition at line 66 of file dependence_graph.h.
|
private |
Definition at line 178 of file dependence_graph.h.
Definition at line 69 of file dependence_graph.h.
|
inlineexplicit |
Definition at line 71 of file dependence_graph.h.
|
private |
Definition at line 54 of file dependence_graph.cpp.
|
private |
Definition at line 150 of file dependence_graph.cpp.
|
inline |
Definition at line 164 of file dependence_graph.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 150 of file dependence_graph.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 136 of file dependence_graph.h.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 122 of file dependence_graph.h.
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 98 of file dependence_graph.h.
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.
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 264 of file dependence_graph.cpp.
|
overridevirtual |
Outputs the current value of the domain.
Reimplemented from ai_domain_baset.
Definition at line 303 of file dependence_graph.cpp.
void dep_graph_domaint::populate_dep_graph | ( | dependence_grapht & | dep_graph, |
goto_programt::const_targett | this_loc | ||
) | const |
Definition at line 378 of file dependence_graph.cpp.
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 195 of file dependence_graph.cpp.
|
friend |
|
friend |
|
private |
Definition at line 187 of file dependence_graph.h.
|
private |
Definition at line 182 of file dependence_graph.h.
|
private |
Definition at line 191 of file dependence_graph.h.
|
private |
Definition at line 176 of file dependence_graph.h.
|
private |
Definition at line 174 of file dependence_graph.h.
|
private |
Definition at line 175 of file dependence_graph.h.