cprover
|
#include <value_set_domain_fi.h>
Public Member Functions | |
virtual void | output (const namespacet &ns, std::ostream &out) const |
virtual void | initialize (const namespacet &ns) |
virtual bool | transform (const namespacet &ns, locationt from_l, locationt to_l) |
virtual void | get_reference_set (const namespacet &ns, const exprt &expr, expr_sett &expr_set) |
virtual void | clear (void) |
![]() | |
flow_insensitive_abstract_domain_baset () | |
virtual | ~flow_insensitive_abstract_domain_baset () |
Public Attributes | |
value_set_fit | value_set |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
typedef std::unordered_set< exprt, irep_hash > | expr_sett |
![]() | |
exprt | get_guard (locationt from, locationt to) const |
exprt | get_return_lhs (locationt to) const |
![]() | |
bool | changed |
Definition at line 20 of file value_set_domain_fi.h.
|
inlinevirtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 58 of file value_set_domain_fi.h.
References value_set_fit::clear(), and value_set.
|
inlinevirtual |
Reimplemented from flow_insensitive_abstract_domain_baset.
Definition at line 50 of file value_set_domain_fi.h.
References value_set_fit::get_reference_set(), and value_set.
|
inlinevirtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 39 of file value_set_domain_fi.h.
References value_set_fit::clear(), and value_set.
|
inlinevirtual |
Reimplemented from flow_insensitive_abstract_domain_baset.
Definition at line 32 of file value_set_domain_fi.h.
References value_set_fit::output(), and value_set.
|
virtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 17 of file value_set_domain_fi.cpp.
References value_set_fit::apply_code(), code_function_callt::arguments(), ASSIGN, value_set_fit::changed, value_set_fit::do_end_function(), value_set_fit::do_function_call(), END_FUNCTION, FUNCTION_CALL, flow_insensitive_abstract_domain_baset::get_return_lhs(), GOTO, OTHER, RETURN, value_set_fit::set_from(), value_set_fit::set_to(), to_code_function_call(), and value_set.
value_set_fit value_set_domain_fit::value_set |
Definition at line 23 of file value_set_domain_fi.h.
Referenced by value_set_analysis_fit::add_vars(), clear(), get_reference_set(), value_set_analysis_fit::get_values(), initialize(), output(), and transform().