cprover
|
#include <value_set_domain_fivrns.h>
Public Member Functions | |
virtual void | output (const namespacet &ns, std::ostream &out) const |
virtual void | initialize (const namespacet &) |
virtual bool | transform (const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, 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_fivrnst | 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_fivrns.h.
|
inlinevirtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 56 of file value_set_domain_fivrns.h.
|
inlinevirtual |
Reimplemented from flow_insensitive_abstract_domain_baset.
Definition at line 48 of file value_set_domain_fivrns.h.
|
inlinevirtual |
Implements flow_insensitive_abstract_domain_baset.
Definition at line 35 of file value_set_domain_fivrns.h.
|
inlinevirtual |
Reimplemented from flow_insensitive_abstract_domain_baset.
Definition at line 28 of file value_set_domain_fivrns.h.
|
virtual |
Implements flow_insensitive_abstract_domain_baset.
value_set_fivrnst value_set_domain_fivrnst::value_set |
Definition at line 24 of file value_set_domain_fivrns.h.