cprover
|
#include <uninitialized_domain.h>
Public Types | |
typedef std::set< irep_idt > | uninitializedt |
![]() | |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
uninitialized_domaint () | |
void | transform (locationt from, locationt 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 |
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 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 &ns) 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'. 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 58 of file uninitialized_domain.cpp.
References index_exprt::array(), irept::id(), member_exprt::struct_op(), to_index_expr(), to_member_expr(), to_symbol_expr(), and uninitialized.
Referenced by transform().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 65 of file uninitialized_domain.h.
References DATA_INVARIANT, has_values, tvt::is_false(), and uninitialized.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 58 of file uninitialized_domain.h.
References DATA_INVARIANT, has_values, tvt::is_true(), and uninitialized.
|
inlinefinaloverridevirtual |
no states
Implements ai_domain_baset.
Definition at line 47 of file uninitialized_domain.h.
References has_values, and uninitialized.
|
inlinefinaloverridevirtual |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 53 of file uninitialized_domain.h.
References 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 41 of file uninitialized_domain.h.
References has_values, and uninitialized.
Referenced by make_entry().
bool uninitialized_domaint::merge | ( | const uninitialized_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 83 of file uninitialized_domain.cpp.
References has_values, tvt::is_false(), uninitialized, and tvt::unknown().
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 68 of file uninitialized_domain.cpp.
References has_values, tvt::is_known(), tvt::to_string(), and uninitialized.
|
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)
"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "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())
Implements ai_domain_baset.
Definition at line 21 of file uninitialized_domain.cpp.
References assign(), DECL, expressions_read(), expressions_written(), code_declt::get_identifier(), has_values, tvt::is_false(), symbolt::is_static_lifetime, namespacet::lookup(), to_code_decl(), and uninitialized.
|
private |
Definition at line 79 of file uninitialized_domain.h.
Referenced by is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), and transform().
uninitializedt uninitialized_domaint::uninitialized |
Definition at line 30 of file uninitialized_domain.h.
Referenced by assign(), is_bottom(), is_top(), make_bottom(), make_top(), merge(), output(), and transform().