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 (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 |
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... | |
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 |
void | set_node_id (node_indext id) |
node_indext | get_node_id () const |
void | populate_dep_graph (dependence_grapht &, goto_programt::const_targett) const |
![]() | |
virtual | ~ai_domain_baset () |
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 (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 |
bool | has_changed |
depst | control_deps |
depst | control_dep_candidates |
depst | data_deps |
Friends | |
const friend depst & | dependence_graph_test_get_control_deps (const dep_graph_domaint &) |
const friend 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'. More... | |
Definition at line 66 of file dependence_graph.h.
|
private |
Definition at line 185 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 55 of file dependence_graph.cpp.
|
private |
Definition at line 153 of file dependence_graph.cpp.
|
inline |
Definition at line 171 of file dependence_graph.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 152 of file dependence_graph.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 138 of file dependence_graph.h.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 124 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 100 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 25 of file dependence_graph.cpp.
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 240 of file dependence_graph.cpp.
|
overridevirtual |
Outputs the current value of the domain.
Reimplemented from ai_domain_baset.
Definition at line 279 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 324 of file dependence_graph.cpp.
|
inline |
Definition at line 166 of file dependence_graph.h.
|
finaloverridevirtual |
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)
"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())
Implements ai_domain_baset.
Definition at line 193 of file dependence_graph.cpp.
|
friend |
|
friend |
|
private |
Definition at line 194 of file dependence_graph.h.
|
private |
Definition at line 189 of file dependence_graph.h.
|
private |
Definition at line 198 of file dependence_graph.h.
|
private |
Definition at line 183 of file dependence_graph.h.
|
private |
Definition at line 181 of file dependence_graph.h.
|
private |
Definition at line 182 of file dependence_graph.h.