This is the domain for a value set analysis. More...
#include <value_set_domain.h>
Inheritance diagram for value_set_domain_templatet< VST >: Collaboration diagram for value_set_domain_templatet< VST >:Public Member Functions | |
| value_set_domain_templatet (locationt l) | |
| void | make_bottom () override |
| no states More... | |
| void | make_top () override |
| all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it. More... | |
| void | make_entry () override |
| Make this domain a reasonable entry-point state For most domains top is sufficient. More... | |
| bool | is_bottom () const override |
| bool | is_top () const override |
| bool | merge (const value_set_domain_templatet< VST > &other, trace_ptrt, trace_ptrt) |
| void | output (std::ostream &out, const ai_baset &, const namespacet &) const override |
| void | transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns) 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 | get_reference_set (const namespacet &ns, const exprt &expr, value_setst::valuest &dest) |
| exprt | get_return_lhs (locationt to) const |
| xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const override |
| Public Member Functions inherited from ai_domain_baset | |
| virtual | ~ai_domain_baset () |
| virtual jsont | output_json (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... | |
Public Attributes | |
| VST | value_set |
Protected Attributes | |
| bool | reachable |
| ait checks whether domains are bottom to increase speed and accuracy. More... | |
Additional Inherited Members | |
| Public Types inherited from ai_domain_baset | |
| typedef goto_programt::const_targett | locationt |
| typedef ai_history_baset::trace_ptrt | trace_ptrt |
| Protected Member Functions inherited from ai_domain_baset | |
| 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... | |
Detailed Description
template<class VST>
class value_set_domain_templatet< VST >
This is the domain for a value set analysis.
It is intended to be the template parameter for value_set_analysis_templatet, so VST would be value_sett.
Definition at line 25 of file value_set_domain.h.
Constructor & Destructor Documentation
◆ value_set_domain_templatet()
|
inlineexplicit |
Definition at line 35 of file value_set_domain.h.
Member Function Documentation
◆ get_reference_set()
|
inline |
Definition at line 90 of file value_set_domain.h.
◆ get_return_lhs()
|
inline |
Definition at line 98 of file value_set_domain.h.
◆ is_bottom()
|
inlineoverridevirtual |
Implements ai_domain_baset.
Definition at line 57 of file value_set_domain.h.
◆ is_top()
|
inlineoverridevirtual |
Implements ai_domain_baset.
Definition at line 62 of file value_set_domain.h.
◆ make_bottom()
|
inlineoverridevirtual |
◆ make_entry()
|
inlineoverridevirtual |
Make this domain a reasonable entry-point state For most domains top is sufficient.
Reimplemented from ai_domain_baset.
Definition at line 52 of file value_set_domain.h.
◆ make_top()
|
inlineoverridevirtual |
all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 47 of file value_set_domain.h.
◆ merge()
|
inline |
Definition at line 70 of file value_set_domain.h.
◆ output()
|
inlineoverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 77 of file value_set_domain.h.
◆ output_xml()
|
inlineoverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 111 of file value_set_domain.h.
◆ transform()
|
overridevirtual |
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 120 of file value_set_domain.h.
Member Data Documentation
◆ reachable
|
protected |
ait checks whether domains are bottom to increase speed and accuracy.
Older frameworks don't so it is necessary to track this.
Definition at line 30 of file value_set_domain.h.
◆ value_set
| VST value_set_domain_templatet< VST >::value_set |
Definition at line 33 of file value_set_domain.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_domain.h
