12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVR_H 13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVR_H 53 out <<
"**** " << it->source_location <<
'\n';
65 void get_globals(std::list<value_set_fivrt::entryt> &dest);
71 std::list<value_set_fivrt::entryt> &dest);
75 const std::string &suffix,
77 std::list<value_set_fivrt::entryt> &dest);
84 std::list<exprt> &dest)
96 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVR_H
The type of an expression.
virtual void initialize(const goto_programt &goto_program)
flow_insensitive_analysist< value_set_domain_fivrt > baset
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrt::entryt > &dest)
void output(const goto_programt &goto_program, std::ostream &out)
void set_from(const irep_idt &function, unsigned inx)
value_set_fivrt value_set
void output(locationt l, std::ostream &out)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void add_vars(const goto_functionst &goto_functions)
unsigned from_target_index
bool check_type(const typet &type)
goto_programt::const_targett locationt
void set_to(const irep_idt &function, unsigned inx)
virtual void get_values(locationt l, const exprt &expr, std::list< exprt > &dest)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
track_optionst track_options
A generic container class for the GOTO intermediate representation of one function.
Value Set (Flow Insensitive, Sharing, Validity Regions)
Flow Insensitive Static Analysis.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Base class for all expressions.
value_set_analysis_fivrt(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
static hash_numbering< irep_idt, irep_id_hash > function_numbering
virtual void output(const namespacet &ns, std::ostream &out) const
void get_globals(std::list< value_set_fivrt::entryt > &dest)
goto_programt & goto_program
void get_entries(const symbolt &symbol, std::list< value_set_fivrt::entryt > &dest)
#define forall_goto_program_instructions(it, program)
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
value_set_domain_fivrt state