cprover
|
#include <flow_insensitive_analysis.h>
Public Types | |
typedef goto_programt::const_targett | locationt |
typedef std::unordered_set< exprt, irep_hash > | expr_sett |
Public Member Functions | |
flow_insensitive_abstract_domain_baset () | |
virtual void | initialize (const namespacet &ns)=0 |
virtual bool | transform (const namespacet &ns, locationt from, locationt to)=0 |
virtual | ~flow_insensitive_abstract_domain_baset () |
virtual void | output (const namespacet &, std::ostream &) const |
virtual void | get_reference_set (const namespacet &, const exprt &, expr_sett &expr_set) |
virtual void | clear (void)=0 |
Protected Member Functions | |
exprt | get_guard (locationt from, locationt to) const |
exprt | get_return_lhs (locationt to) const |
Protected Attributes | |
bool | changed |
Definition at line 25 of file flow_insensitive_analysis.h.
typedef std::unordered_set<exprt, irep_hash> flow_insensitive_abstract_domain_baset::expr_sett |
Definition at line 52 of file flow_insensitive_analysis.h.
Definition at line 33 of file flow_insensitive_analysis.h.
|
inline |
Definition at line 28 of file flow_insensitive_analysis.h.
|
inlinevirtual |
Definition at line 42 of file flow_insensitive_analysis.h.
|
pure virtual |
Implemented in value_set_domain_fit, value_set_domain_fivrnst, and value_set_domain_fivrt.
|
protected |
Definition at line 20 of file flow_insensitive_analysis.cpp.
References exprt::make_not().
|
inlinevirtual |
Reimplemented in value_set_domain_fit, value_set_domain_fivrnst, and value_set_domain_fivrt.
Definition at line 54 of file flow_insensitive_analysis.h.
Definition at line 40 of file flow_insensitive_analysis.cpp.
References get_nil_irep(), code_function_callt::lhs(), and to_code_function_call().
Referenced by value_set_domain_fivrt::transform(), value_set_domain_fivrnst::transform(), and value_set_domain_fit::transform().
|
pure virtual |
Implemented in value_set_domain_fit, value_set_domain_fivrnst, and value_set_domain_fivrt.
|
inlinevirtual |
Reimplemented in value_set_domain_fit, value_set_domain_fivrnst, and value_set_domain_fivrt.
Definition at line 46 of file flow_insensitive_analysis.h.
Referenced by flow_insensitive_analysis_baset::output().
|
pure virtual |
Implemented in value_set_domain_fit, value_set_domain_fivrnst, and value_set_domain_fivrt.
Referenced by flow_insensitive_analysis_baset::do_function_call(), and flow_insensitive_analysis_baset::visit().
|
protected |
Definition at line 66 of file flow_insensitive_analysis.h.