CBMC
|
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.