|
| dep_graph_domaint (node_indext id) |
|
bool | merge (const dep_graph_domaint &src, trace_ptrt from, trace_ptrt 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)
|
|
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.
|
|
void | make_top () final override |
| all states – the analysis doesn't use this, and domains may refuse to implement it.
|
|
void | make_bottom () final override |
| no states
|
|
void | make_entry () final override |
| Make this domain a reasonable entry-point state.
|
|
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 |
|
Public Member Functions inherited from ai_domain_baset |
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)=0 |
| 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)
|
|
virtual void | output (std::ostream &, const ai_baset &, const namespacet &) const |
|
virtual jsont | output_json (const ai_baset &ai, const namespacet &ns) const |
|
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
|
virtual void | make_bottom ()=0 |
| no states
|
|
virtual void | make_top ()=0 |
| all states – the analysis doesn't use this, and domains may refuse to implement it.
|
|
virtual void | make_entry ()=0 |
| Make this domain a reasonable entry-point state.
|
|
virtual bool | is_bottom () const =0 |
|
virtual bool | is_top () const =0 |
|
virtual bool | ai_simplify (exprt &condition, const namespacet &) const |
| also add
|
|
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
| Simplifies the expression but keeps it as an l-value.
|
|
virtual exprt | to_predicate (void) const |
| Gives a Boolean condition that is true for all values represented by the domain.
|
|
Definition at line 66 of file dependence_graph.h.
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.