cprover
|
#include <value_set_domain_fivr.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_fivrt | 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_fivr.h.
|
inlinevirtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 53 of file value_set_domain_fivr.h.
References value_set_fivrt::clear(), and value_set.
|
inlinevirtual |
Reimplemented from flow_insensitive_abstract_domain_baset.
Definition at line 45 of file value_set_domain_fivr.h.
References value_set_fivrt::get_reference_set(), and value_set.
|
inlinevirtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 34 of file value_set_domain_fivr.h.
References value_set_fivrt::clear(), and value_set.
|
inlinevirtual |
Reimplemented from flow_insensitive_abstract_domain_baset.
Definition at line 27 of file value_set_domain_fivr.h.
References value_set_fivrt::output(), and value_set.
Referenced by value_set_analysis_fivrt::output().
|
virtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 17 of file value_set_domain_fivr.cpp.
References value_set_fivrt::apply_code(), code_function_callt::arguments(), ASSIGN, value_set_fivrt::do_end_function(), value_set_fivrt::do_function_call(), END_FUNCTION, FUNCTION_CALL, flow_insensitive_abstract_domain_baset::get_return_lhs(), value_set_fivrt::handover(), OTHER, RETURN, value_set_fivrt::set_from(), value_set_fivrt::set_to(), to_code_function_call(), and value_set.
value_set_fivrt value_set_domain_fivrt::value_set |
Definition at line 23 of file value_set_domain_fivr.h.
Referenced by value_set_analysis_fivrt::add_vars(), clear(), get_reference_set(), value_set_analysis_fivrt::get_values(), initialize(), output(), value_set_analysis_fivrt::output(), and transform().