|
CBMC
|
Include dependency graph for value_set_analysis.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| 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. More... | |
Macros | |
| #define | USE_DEPRECATED_STATIC_ANALYSIS_H |
Typedefs | |
| typedef value_set_analysis_templatet< value_set_domain_templatet< value_sett > > | value_set_analysist |
Functions | |
| void | value_sets_to_xml (const std::function< const value_sett &(goto_programt::const_targett)> &get_value_set, const goto_programt &goto_program, xmlt &dest) |
| void | convert (const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest) |
| void | convert (const goto_programt &goto_program, const value_set_analysist &value_set_analysis, xmlt &dest) |
Value Set Propagation
Definition in file value_set_analysis.h.
| #define USE_DEPRECATED_STATIC_ANALYSIS_H |
Definition at line 15 of file value_set_analysis.h.
Definition at line 77 of file value_set_analysis.h.
| void convert | ( | const goto_functionst & | goto_functions, |
| const value_set_analysist & | value_set_analysis, | ||
| xmlt & | dest | ||
| ) |
Definition at line 68 of file value_set_analysis.cpp.
| void convert | ( | const goto_programt & | goto_program, |
| const value_set_analysist & | value_set_analysis, | ||
| xmlt & | dest | ||
| ) |
Definition at line 86 of file value_set_analysis.cpp.
| void value_sets_to_xml | ( | const std::function< const value_sett &(goto_programt::const_targett)> & | get_value_set, |
| const goto_programt & | goto_program, | ||
| xmlt & | dest | ||
| ) |
Definition at line 16 of file value_set_analysis.cpp.