Go to the documentation of this file.
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
45 void get_globals(std::list<value_set_fit::entryt> &dest);
51 std::list<value_set_fit::entryt> &dest);
55 const std::string &suffix,
57 std::list<value_set_fit::entryt> &dest);
61 DEPRECATED(
SINCE(2019, 05, 22,
"Use the version returning list instead"))
66 std::list<
exprt> &dest)
override
80 const exprt &expr)
override;
83 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
goto_programt::const_targett locationt
static hash_numbering< irep_idt, irep_id_hash > function_numbering
flow_insensitive_analysist< value_set_domain_fit > baset
The type of an expression, extends irept.
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
value_set_analysis_fit(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
Base class for all expressions.
unsigned from_target_index
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void initialize(const goto_programt &goto_program) override
Value Set (Flow Insensitive)
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
void get_globals(std::list< value_set_fit::entryt > &dest)
Flow Insensitive Static Analysis.
#define SINCE(year, month, day, msg)
bool check_type(const typet &type)
@ TRACK_FUNCTION_POINTERS
value_set_domain_fit state
A collection of goto functions.
goto_programt::const_targett locationt
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
A generic container class for the GOTO intermediate representation of one function.
void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest) override
track_optionst track_options
void add_vars(const goto_functionst &goto_functions)