|
CBMC
|
#include <flow_insensitive_analysis.h>
Inheritance diagram for flow_insensitive_analysist< T >:
Collaboration diagram for flow_insensitive_analysist< T >:Public Types | |
| typedef goto_programt::const_targett | locationt |
Public Types inherited from flow_insensitive_analysis_baset | |
| typedef flow_insensitive_abstract_domain_baset | statet |
| typedef goto_programt::const_targett | locationt |
Public Member Functions | |
| flow_insensitive_analysist (const namespacet &_ns) | |
| virtual void | clear () |
| T & | get_data () |
| const T & | get_data () const |
Public Member Functions inherited from flow_insensitive_analysis_baset | |
| 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 | 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) |
Protected Member Functions | |
| virtual statet & | get_state () |
| virtual const statet & | get_state () const |
| void | get_reference_set (const exprt &expr, expr_sett &expr_set) |
Protected Member Functions inherited from flow_insensitive_analysis_baset | |
| locationt | get_next (working_sett &working_set) |
| void | put_in_working_set (working_sett &working_set, locationt l) |
| bool | fixedpoint (const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions) |
| void | fixedpoint (const goto_functionst &goto_functions) |
| bool | visit (const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions) |
| bool | do_function_call_rec (const irep_idt &calling_function, locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions) |
| bool | do_function_call (const irep_idt &calling_function, locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state) |
Protected Attributes | |
| T | state |
Protected Attributes inherited from flow_insensitive_analysis_baset | |
| const namespacet & | ns |
| functions_donet | functions_done |
| recursion_sett | recursion_set |
| bool | initialized |
Private Member Functions | |
| void | dummy (const T &s) |
Additional Inherited Members | |
Public Attributes inherited from flow_insensitive_analysis_baset | |
| std::set< locationt > | seen_locations |
| std::map< locationt, unsigned > | statistics |
Protected Types inherited from flow_insensitive_analysis_baset | |
| typedef std::priority_queue< locationt > | 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 inherited from flow_insensitive_analysis_baset | |
| static locationt | successor (locationt l) |
Definition at line 231 of file flow_insensitive_analysis.h.
| typedef goto_programt::const_targett flow_insensitive_analysist< T >::locationt |
Definition at line 240 of file flow_insensitive_analysis.h.
|
inlineexplicit |
Definition at line 235 of file flow_insensitive_analysis.h.
|
inlinevirtual |
Reimplemented from flow_insensitive_analysis_baset.
Definition at line 242 of file flow_insensitive_analysis.h.
|
inlineprivate |
Definition at line 267 of file flow_insensitive_analysis.h.
|
inline |
Definition at line 248 of file flow_insensitive_analysis.h.
|
inline |
Definition at line 249 of file flow_insensitive_analysis.h.
|
inlineprotectedvirtual |
Implements flow_insensitive_analysis_baset.
Definition at line 258 of file flow_insensitive_analysis.h.
|
inlineprotectedvirtual |
Implements flow_insensitive_analysis_baset.
Definition at line 254 of file flow_insensitive_analysis.h.
|
inlineprotectedvirtual |
Implements flow_insensitive_analysis_baset.
Definition at line 256 of file flow_insensitive_analysis.h.
|
protected |
Definition at line 252 of file flow_insensitive_analysis.h.