value_set_analysis_templatet< VSDT > Class Template Reference
This template class implements a data-flow analysis which keeps track of what values different variables might have at different points in the program. More...
#include <value_set_analysis.h>
Inheritance diagram for value_set_analysis_templatet< VSDT >: Collaboration diagram for value_set_analysis_templatet< VSDT >:Public Types | |
| typedef VSDT | domaint |
| typedef static_analysist< domaint > | baset |
| typedef baset::locationt | locationt |
| Public Types inherited from value_setst | |
| typedef std::list< exprt > | valuest |
| Public Types inherited from static_analysist< VSDT > | |
| typedef goto_programt::const_targett | locationt |
| Public Types inherited from static_analysis_baset | |
| typedef domain_baset | statet |
| typedef goto_programt::const_targett | locationt |
Public Member Functions | |
| value_set_analysis_templatet (const namespacet &ns) | |
| const value_sett & | get_value_set (goto_programt::const_targett t) |
| void | convert (const goto_programt &goto_program, xmlt &dest) const |
| std::vector< exprt > | get_values (const irep_idt &, locationt l, const exprt &expr) override |
| Public Member Functions inherited from value_setst | |
| value_setst () | |
| virtual | ~value_setst () |
| Public Member Functions inherited from static_analysist< VSDT > | |
| static_analysist (const namespacet &_ns) | |
| VSDT & | operator[] (locationt l) |
| const VSDT & | operator[] (locationt l) const |
| virtual void | clear () |
| virtual bool | has_location (locationt l) const |
| Public Member Functions inherited from static_analysis_baset | |
| static_analysis_baset (const namespacet &_ns) | |
| virtual void | initialize (const goto_programt &goto_program) |
| virtual void | initialize (const goto_functionst &goto_functions) |
| virtual void | update (const goto_programt &goto_program) |
| virtual void | update (const goto_functionst &goto_functions) |
| virtual void | operator() (const irep_idt &function_identifier, const goto_programt &goto_program) |
| virtual void | operator() (const goto_functionst &goto_functions) |
| virtual | ~static_analysis_baset () |
| virtual void | output (const goto_functionst &goto_functions, std::ostream &out) const |
| void | output (const goto_programt &goto_program, std::ostream &out) const |
| void | insert (locationt l) |
Additional Inherited Members | |
| Static Public Member Functions inherited from static_analysis_baset | |
| static exprt | get_guard (locationt from, locationt to) |
| static exprt | get_return_lhs (locationt to) |
| Protected Types inherited from static_analysist< VSDT > | |
| typedef std::map< locationt, VSDT > | state_mapt |
| Protected Types inherited from static_analysis_baset | |
| typedef std::map< unsigned, locationt > | working_sett |
| typedef std::set< irep_idt > | functions_donet |
| typedef std::set< irep_idt > | recursion_sett |
| typedef domain_baset::expr_sett | expr_sett |
| Protected Member Functions inherited from static_analysist< VSDT > | |
| virtual statet & | get_state (locationt l) |
| virtual const statet & | get_state (locationt l) const |
| virtual bool | merge (statet &a, const statet &b, locationt to) |
| virtual std::unique_ptr< statet > | make_temporary_state (statet &s) |
| virtual void | generate_state (locationt l) |
| virtual void | get_reference_set (locationt l, const exprt &expr, std::list< exprt > &dest) |
| virtual void | fixedpoint (const goto_functionst &goto_functions) |
| Protected Member Functions inherited from static_analysis_baset | |
| virtual void | output (const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
| locationt | get_next (working_sett &working_set) |
| void | put_in_working_set (working_sett &working_set, locationt l) |
| bool | fixedpoint (const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions) |
| void | sequential_fixedpoint (const goto_functionst &goto_functions) |
| void | concurrent_fixedpoint (const goto_functionst &goto_functions) |
| bool | visit (const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions) |
| void | generate_states (const goto_functionst &goto_functions) |
| void | generate_states (const goto_programt &goto_program) |
| void | do_function_call_rec (const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions) |
| void | do_function_call (const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state) |
| Static Protected Member Functions inherited from static_analysis_baset | |
| static locationt | successor (locationt l) |
| Protected Attributes inherited from static_analysist< VSDT > | |
| state_mapt | state_map |
| Protected Attributes inherited from static_analysis_baset | |
| const namespacet & | ns |
| functions_donet | functions_done |
| recursion_sett | recursion_set |
| bool | initialized |
Detailed Description
template<class VSDT>
class value_set_analysis_templatet< VSDT >
This template class implements a data-flow analysis which keeps track of what values different variables might have at different points in the program.
It is used through the alias value_set_analysist, so VSDT is value_set_domain_templatet<value_sett>.
Note: it is currently based on static_analysist, which is obsolete. It should be moved onto ait.
Definition at line 37 of file value_set_analysis.h.
Member Typedef Documentation
◆ baset
template<class VSDT >
| typedef static_analysist<domaint> value_set_analysis_templatet< VSDT >::baset |
Definition at line 43 of file value_set_analysis.h.
◆ domaint
template<class VSDT >
| typedef VSDT value_set_analysis_templatet< VSDT >::domaint |
Definition at line 42 of file value_set_analysis.h.
◆ locationt
template<class VSDT >
| typedef baset::locationt value_set_analysis_templatet< VSDT >::locationt |
Definition at line 44 of file value_set_analysis.h.
Constructor & Destructor Documentation
◆ value_set_analysis_templatet()
template<class VSDT >
|
inlineexplicit |
Definition at line 46 of file value_set_analysis.h.
Member Function Documentation
◆ convert()
template<class VSDT >
|
inline |
Definition at line 55 of file value_set_analysis.h.
◆ get_value_set()
template<class VSDT >
|
inline |
Definition at line 50 of file value_set_analysis.h.
◆ get_values()
template<class VSDT >
|
inlineoverridevirtual |
Implements value_setst.
Definition at line 69 of file value_set_analysis.h.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/pointer-analysis/value_set_analysis.h
