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 |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final |
void | make_top () final |
void | make_bottom () final |
void | make_entry () final |
bool | merge (const uninitialized_domaint &other, locationt from, locationt to) |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
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 |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Use the information in the domain to simplify the expression on the LHS of an assignment. More... | |
Public Attributes | |
uninitializedt | uninitialized |
Private Member Functions | |
void | assign (const exprt &lhs) |
Private Attributes | |
tvt | has_values |
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.
References index_exprt::array(), irept::id(), member_exprt::struct_op(), to_index_expr(), to_member_expr(), to_symbol_expr(), and uninitialized.
Referenced by transform().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 49 of file uninitialized_domain.h.
References has_values.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 55 of file uninitialized_domain.h.
References make_top(), and merge().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 43 of file uninitialized_domain.h.
References has_values.
Referenced by make_entry().
bool uninitialized_domaint::merge | ( | const uninitialized_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 79 of file uninitialized_domain.cpp.
References has_values, tvt::is_false(), uninitialized, and tvt::unknown().
Referenced by make_entry().
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 64 of file uninitialized_domain.cpp.
References has_values, tvt::is_known(), tvt::to_string(), and uninitialized.
|
final |
Definition at line 19 of file uninitialized_domain.cpp.
References assign(), DECL, expressions_read(), expressions_written(), forall_expr_list, code_declt::get_identifier(), has_values, tvt::is_false(), symbolt::is_static_lifetime, namespacet::lookup(), to_code_decl(), and uninitialized.
|
private |
Definition at line 67 of file uninitialized_domain.h.
Referenced by make_bottom(), make_top(), merge(), output(), and transform().
uninitializedt uninitialized_domaint::uninitialized |
Definition at line 30 of file uninitialized_domain.h.
Referenced by assign(), merge(), output(), and transform().