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 49 [
this](
locationt l) {
return (*
this)[l].value_set; },
62 (*this)[l].value_set.get_value_set(expr, dest,
baset::ns);
80 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
value_set_analysis_templatet(const namespacet &ns)
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)
baset::locationt locationt
goto_programt::const_targett locationt
instructionst::const_iterator const_targett
goto_programt::const_targett locationt
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
void convert(const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest) const
void value_sets_to_xml(std::function< const value_sett &(goto_programt::const_targett)> get_value_set, const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest)
std::list< exprt > valuest
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist