CBMC
|
#include <flow_insensitive_analysis.h>
Public Types | |
typedef flow_insensitive_abstract_domain_baset | statet |
typedef goto_programt::const_targett | locationt |
Public Member Functions | |
bool | seen (const locationt &l) |
flow_insensitive_analysis_baset (const namespacet &_ns) | |
virtual void | initialize (const goto_programt &) |
virtual void | initialize (const goto_functionst &) |
virtual void | update (const goto_programt &goto_program) |
virtual void | update (const goto_functionst &goto_functions) |
virtual void | operator() (const irep_idt &function_id, const goto_programt &goto_program) |
virtual void | operator() (const goto_functionst &goto_functions) |
virtual | ~flow_insensitive_analysis_baset () |
virtual void | clear () |
virtual void | output (const goto_functionst &goto_functions, std::ostream &out) |
virtual void | output (const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) |
Public Attributes | |
std::set< locationt, goto_programt::target_less_than > | seen_locations |
std::map< locationt, unsigned, goto_programt::target_less_than > | statistics |
Protected Types | |
typedef std::priority_queue< locationt, std::vector< locationt >, goto_programt::target_less_than > | working_sett |
typedef std::set< irep_idt > | functions_donet |
typedef std::set< irep_idt > | recursion_sett |
typedef flow_insensitive_abstract_domain_baset::expr_sett | expr_sett |
Static Protected Member Functions | |
static locationt | successor (locationt l) |
Protected Attributes | |
const namespacet & | ns |
functions_donet | functions_done |
recursion_sett | recursion_set |
bool | initialized |
Definition at line 90 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 226 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 196 of file flow_insensitive_analysis.h.
Definition at line 94 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 199 of file flow_insensitive_analysis.h.
Definition at line 93 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 162 of file flow_insensitive_analysis.h.
|
inlineexplicit |
Definition at line 105 of file flow_insensitive_analysis.h.
|
inlinevirtual |
Definition at line 137 of file flow_insensitive_analysis.h.
Reimplemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.
Definition at line 141 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 190 of file flow_insensitive_analysis.cpp.
|
protected |
Definition at line 273 of file flow_insensitive_analysis.cpp.
|
protected |
Definition at line 379 of file flow_insensitive_analysis.cpp.
|
protected |
Definition at line 96 of file flow_insensitive_analysis.cpp.
|
protected |
Definition at line 80 of file flow_insensitive_analysis.cpp.
|
protectedpure virtual |
Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.
Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.
Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.
|
inlinevirtual |
Reimplemented in value_set_analysis_fit.
Definition at line 119 of file flow_insensitive_analysis.h.
|
inlinevirtual |
Reimplemented in value_set_analysis_fit.
Definition at line 111 of file flow_insensitive_analysis.h.
|
virtual |
Definition at line 43 of file flow_insensitive_analysis.cpp.
|
virtual |
Definition at line 50 of file flow_insensitive_analysis.cpp.
|
virtual |
Definition at line 58 of file flow_insensitive_analysis.cpp.
|
virtual |
Definition at line 71 of file flow_insensitive_analysis.cpp.
|
inlineprotected |
Definition at line 166 of file flow_insensitive_analysis.h.
Definition at line 100 of file flow_insensitive_analysis.h.
Definition at line 190 of file flow_insensitive_analysis.h.
|
virtual |
Definition at line 394 of file flow_insensitive_analysis.cpp.
|
virtual |
Definition at line 399 of file flow_insensitive_analysis.cpp.
|
protected |
Definition at line 125 of file flow_insensitive_analysis.cpp.
|
protected |
Definition at line 197 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 202 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 156 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 200 of file flow_insensitive_analysis.h.
std::set<locationt, goto_programt::target_less_than> flow_insensitive_analysis_baset::seen_locations |
Definition at line 96 of file flow_insensitive_analysis.h.
std::map<locationt, unsigned, goto_programt::target_less_than> flow_insensitive_analysis_baset::statistics |
Definition at line 98 of file flow_insensitive_analysis.h.