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, 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 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 |
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 (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 52 of file dependence_graph.cpp.
|
private |
Definition at line 148 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 22 of file dependence_graph.cpp.
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 265 of file dependence_graph.cpp.
|
overridevirtual |
Outputs the current value of the domain.
Reimplemented from ai_domain_baset.
Definition at line 304 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 379 of file dependence_graph.cpp.
|
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)
in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after
"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())
The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature
Implements ai_domain_baset.
Definition at line 193 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.