13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
58 out <<
"**** " << it->source_location <<
'\n';
59 output(function_id, it, out);
76 std::list<value_set_fivrnst::entryt> &
dest);
80 const std::string &suffix,
82 std::list<value_set_fivrnst::entryt> &
dest);
90 std::list<exprt> &
dest)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
value_set_domain_fivrnst state
goto_programt::const_targett locationt
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
void get_globals(std::list< value_set_fivrnst::entryt > &dest)
track_optionst track_options
virtual void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest)
flow_insensitive_analysist< value_set_domain_fivrnst > baset
void output(const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out)
void get_entries(const symbolt &symbol, std::list< value_set_fivrnst::entryt > &dest)
void add_vars(const goto_functionst &goto_functions)
void output(const irep_idt &function_id, locationt l, std::ostream &out)
value_set_analysis_fivrnst(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
void add_vars(const goto_programt &goto_programa)
virtual void initialize(const goto_functionst &goto_functions)
virtual void initialize(const goto_programt &goto_program)
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrnst::entryt > &dest)
@ TRACK_FUNCTION_POINTERS
bool check_type(const typet &type)
value_set_fivrnst value_set
virtual void output(const namespacet &ns, std::ostream &out) const
static numberingt< irep_idt > function_numbering
void set_to(const irep_idt &function, unsigned inx)
void set_from(const irep_idt &function, unsigned inx)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
unsigned from_target_index
Flow Insensitive Static Analysis.
#define forall_goto_program_instructions(it, program)
Value Set Domain (Flow Insensitive, Validity Regions)