#include <uninitialized_domain.h>
Inheritance diagram for uninitialized_domaint: Collaboration diagram for uninitialized_domaint:Public Types | |
| typedef std::set< irep_idt > | uninitializedt |
| Public Types inherited from ai_domain_baset | |
| typedef goto_programt::const_targett | locationt |
| typedef ai_history_baset::trace_ptrt | trace_ptrt |
Public Member Functions | |
| uninitialized_domaint () | |
| 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 |
| 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 override final |
| bool | is_bottom () const override final |
| bool | merge (const uninitialized_domaint &other, trace_ptrt from, trace_ptrt to) |
| 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 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... | |
Public Attributes | |
| uninitializedt | uninitialized |
Private Member Functions | |
| void | assign (const exprt &lhs) |
Private Attributes | |
| tvt | has_values |
Additional Inherited Members | |
| 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
Definition at line 21 of file uninitialized_domain.h.
Member Typedef Documentation
◆ uninitializedt
| typedef std::set<irep_idt> uninitialized_domaint::uninitializedt |
Definition at line 29 of file uninitialized_domain.h.
Constructor & Destructor Documentation
◆ uninitialized_domaint()
|
inline |
Definition at line 24 of file uninitialized_domain.h.
Member Function Documentation
◆ assign()
|
private |
Definition at line 55 of file uninitialized_domain.cpp.
◆ is_bottom()
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 69 of file uninitialized_domain.h.
◆ is_top()
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 62 of file uninitialized_domain.h.
◆ make_bottom()
|
inlinefinaloverridevirtual |
◆ make_entry()
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 57 of file uninitialized_domain.h.
◆ make_top()
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 45 of file uninitialized_domain.h.
◆ merge()
| bool uninitialized_domaint::merge | ( | const uninitialized_domaint & | other, |
| trace_ptrt | from, | ||
| trace_ptrt | to | ||
| ) |
- Returns
- returns true iff there is something new
Definition at line 80 of file uninitialized_domain.cpp.
◆ output()
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 65 of file uninitialized_domain.cpp.
◆ transform()
|
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 20 of file uninitialized_domain.cpp.
Member Data Documentation
◆ has_values
|
private |
Definition at line 81 of file uninitialized_domain.h.
◆ uninitialized
| uninitializedt uninitialized_domaint::uninitialized |
Definition at line 30 of file uninitialized_domain.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/uninitialized_domain.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/uninitialized_domain.cpp
