cprover
|
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>
Public Types | |
typedef VSDT | domaint |
typedef static_analysist< domaint > | baset |
typedef baset::locationt | locationt |
![]() | |
typedef std::list< exprt > | valuest |
![]() | |
typedef goto_programt::const_targett | locationt |
![]() | |
typedef domain_baset | statet |
typedef goto_programt::const_targett | locationt |
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.
Definition at line 43 of file value_set_analysis.h.
Definition at line 42 of file value_set_analysis.h.
typedef baset::locationt value_set_analysis_templatet< VSDT >::locationt |
Definition at line 44 of file value_set_analysis.h.
|
inlineexplicit |
Definition at line 46 of file value_set_analysis.h.
|
inline |
Definition at line 55 of file value_set_analysis.h.
|
inline |
Definition at line 50 of file value_set_analysis.h.
|
inlineoverridevirtual |
Implements value_setst.
Definition at line 69 of file value_set_analysis.h.