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
52 return (*
this)[t].value_set;
59 using std::placeholders::_1;
71 return (*
this)[l].value_set.get_value_set(expr, baset::ns);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
goto_programt::const_targett locationt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
This template class implements a data-flow analysis which keeps track of what values different variab...
const value_sett & get_value_set(goto_programt::const_targett t)
void convert(const goto_programt &goto_program, xmlt &dest) const
baset::locationt locationt
value_set_analysis_templatet(const namespacet &ns)
static_analysist< domaint > baset
std::vector< exprt > get_values(const irep_idt &, locationt l, const exprt &expr) override
State type in value_set_domaint, used in value-set analysis and goto-symex.
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
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)