cprover
|
#include <value_set_domain.h>
Public Member Functions | |
bool | merge (const value_set_domaint &other, locationt to) |
virtual void | output (const namespacet &ns, std::ostream &out) const |
virtual void | initialize (const namespacet &ns, locationt l) |
virtual void | transform (const namespacet &ns, locationt from_l, locationt to_l) |
virtual void | get_reference_set (const namespacet &ns, const exprt &expr, value_setst::valuest &dest) |
![]() | |
domain_baset () | |
virtual | ~domain_baset () |
virtual void | transform (const namespacet &ns, locationt from, locationt to)=0 |
Public Attributes | |
value_sett | value_set |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
typedef std::unordered_set< exprt, irep_hash > | expr_sett |
![]() | |
bool | seen |
Definition at line 20 of file value_set_domain.h.
|
inlinevirtual |
Reimplemented from domain_baset.
Definition at line 52 of file value_set_domain.h.
References value_sett::get_reference_set().
|
inlinevirtual |
Reimplemented from domain_baset.
Definition at line 39 of file value_set_domain.h.
References value_sett::clear(), value_sett::location_number, and transform().
|
inline |
Definition at line 27 of file value_set_domain.h.
References value_sett::make_union(), and value_set.
|
inlinevirtual |
Reimplemented from domain_baset.
Definition at line 32 of file value_set_domain.h.
References value_sett::output().
|
virtual |
Definition at line 16 of file value_set_domain.cpp.
References value_sett::apply_code(), code_function_callt::arguments(), ASSIGN, ASSUME, DECL, value_sett::do_end_function(), value_sett::do_function_call(), END_FUNCTION, FUNCTION_CALL, static_analysis_baset::get_return_lhs(), GOTO, value_sett::guard(), OTHER, RETURN, to_code_function_call(), and value_set.
Referenced by initialize().
value_sett value_set_domaint::value_set |
Definition at line 23 of file value_set_domain.h.
Referenced by merge(), and transform().