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
value_set_analysis_templatet(const namespacet &ns)
void convert(const goto_programt &goto_program, xmlt &dest) const
virtual void get_values(locationt l, const exprt &expr, value_setst::valuest &dest)
static_analysist< domaint > baset
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)
baset::locationt locationt
goto_programt::const_targett locationt
instructionst::const_iterator const_targett
goto_programt::const_targett locationt
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)
State type in value_set_domaint, used in value-set analysis and goto-symex.
A generic container class for the GOTO intermediate representation of one function.
Base class for all expressions.
goto_programt & goto_program
std::list< exprt > valuest
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist