Go to the documentation of this file.
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
15 #define USE_DEPRECATED_STATIC_ANALYSIS_H
45 return (*
this)[t].value_set;
52 using std::placeholders::_1;
66 (*this)[l].value_set.get_value_set(expr, dest,
baset::ns);
84 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
virtual void get_values(locationt l, const exprt &expr, value_setst::valuest &dest)
void convert(const goto_programt &goto_program, xmlt &dest) const
State type in value_set_domaint, used in value-set analysis and goto-symex.
Base class for all expressions.
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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)
static_analysist< domaint > baset
std::list< exprt > valuest
goto_programt::const_targett locationt
baset::locationt locationt
goto_programt::const_targett locationt
A collection of goto functions.
value_set_analysis_templatet(const namespacet &ns)
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
const value_sett & get_value_set(goto_programt::const_targett t)