cprover
|
#include <uninitialized_domain.h>
Public Types | |
typedef std::set< irep_idt > | uninitializedt |
![]() | |
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, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override |
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, locationt from, locationt to) |
![]() | |
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) |
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... | |
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 | |
![]() | |
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 21 of file uninitialized_domain.h.
typedef std::set<irep_idt> uninitialized_domaint::uninitializedt |
Definition at line 29 of file uninitialized_domain.h.
|
inline |
Definition at line 24 of file uninitialized_domain.h.
|
private |
Definition at line 54 of file uninitialized_domain.cpp.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 69 of file uninitialized_domain.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 62 of file uninitialized_domain.h.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 57 of file uninitialized_domain.h.
|
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.
bool uninitialized_domaint::merge | ( | const uninitialized_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 79 of file uninitialized_domain.cpp.
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 64 of file uninitialized_domain.cpp.
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 21 of file uninitialized_domain.cpp.
|
private |
Definition at line 83 of file uninitialized_domain.h.
uninitializedt uninitialized_domaint::uninitialized |
Definition at line 30 of file uninitialized_domain.h.