value_set_analysis_fit Class Reference

#include <value_set_analysis_fi.h>

+ Inheritance diagram for value_set_analysis_fit:
+ Collaboration diagram for value_set_analysis_fit:

Public Types

typedef flow_insensitive_analysist< value_set_domain_fitbaset
- Public Types inherited from value_setst
typedef std::list< exprtvaluest
- Public Types inherited from flow_insensitive_analysist< value_set_domain_fit >
typedef goto_programt::const_targett locationt
- Public Types inherited from flow_insensitive_analysis_baset
typedef flow_insensitive_abstract_domain_baset statet
typedef goto_programt::const_targett locationt

Public Member Functions

 value_set_analysis_fit (const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
void initialize (const goto_programt &goto_program) override
void initialize (const goto_functionst &goto_functions) override
void get_values (const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest) override
- Public Member Functions inherited from value_setst
 value_setst ()
virtual ~value_setst ()
- Public Member Functions inherited from flow_insensitive_analysist< value_set_domain_fit >
 flow_insensitive_analysist (const namespacet &_ns)
virtual void clear ()
value_set_domain_fitget_data ()
const value_set_domain_fitget_data () const
- Public Member Functions inherited from flow_insensitive_analysis_baset
bool seen (const locationt &l)
 flow_insensitive_analysis_baset (const namespacet &_ns)
virtual void update (const goto_programt &goto_program)
virtual void update (const goto_functionst &goto_functions)
virtual void operator() (const irep_idt &function_id, const goto_programt &goto_program)
virtual void operator() (const goto_functionst &goto_functions)
virtual ~flow_insensitive_analysis_baset ()
virtual void output (const goto_functionst &goto_functions, std::ostream &out)
virtual void output (const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out)

Protected Member Functions

bool check_type (const typet &type)
void get_globals (std::list< value_set_fit::entryt > &dest)
void add_vars (const goto_functionst &goto_functions)
void add_vars (const goto_programt &goto_programa)
void get_entries (const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
void get_entries_rec (const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
- Protected Member Functions inherited from flow_insensitive_analysist< value_set_domain_fit >
virtual statetget_state ()
virtual const statetget_state () const
void get_reference_set (const exprt &expr, expr_sett &expr_set)
- Protected Member Functions inherited from flow_insensitive_analysis_baset
locationt get_next (working_sett &working_set)
void put_in_working_set (working_sett &working_set, locationt l)
bool fixedpoint (const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool fixedpoint (goto_functionst::function_mapt::const_iterator it, const goto_functionst &goto_functions)
void fixedpoint (const goto_functionst &goto_functions)
bool visit (const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool do_function_call_rec (const irep_idt &calling_function, locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
bool do_function_call (const irep_idt &calling_function, locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)

Protected Attributes

track_optionst track_options
- Protected Attributes inherited from flow_insensitive_analysist< value_set_domain_fit >
value_set_domain_fit state
- Protected Attributes inherited from flow_insensitive_analysis_baset
const namespacetns
functions_donet functions_done
recursion_sett recursion_set
bool initialized

Additional Inherited Members

- Public Attributes inherited from flow_insensitive_analysis_baset
std::set< locationtseen_locations
std::map< locationt, unsigned > statistics
- Protected Types inherited from flow_insensitive_analysis_baset
typedef std::priority_queue< locationtworking_sett
typedef std::set< irep_idtfunctions_donet
typedef std::set< irep_idtrecursion_sett
typedef flow_insensitive_abstract_domain_baset::expr_sett expr_sett
- Static Protected Member Functions inherited from flow_insensitive_analysis_baset
static locationt successor (locationt l)

Detailed Description

Definition at line 20 of file value_set_analysis_fi.h.

Member Typedef Documentation

◆ baset

Member Enumeration Documentation

◆ track_optionst


Definition at line 25 of file value_set_analysis_fi.h.

Constructor & Destructor Documentation

◆ value_set_analysis_fit()

value_set_analysis_fit::value_set_analysis_fit ( const namespacet _ns,
track_optionst  _track_options = TRACK_ALL_POINTERS 

Definition at line 28 of file value_set_analysis_fi.h.

Member Function Documentation

◆ add_vars() [1/2]

void value_set_analysis_fit::add_vars ( const goto_functionst goto_functions)

Definition at line 118 of file value_set_analysis_fi.cpp.

◆ add_vars() [2/2]

void value_set_analysis_fit::add_vars ( const goto_programt goto_programa)

Definition at line 36 of file value_set_analysis_fi.cpp.

◆ check_type()

bool value_set_analysis_fit::check_type ( const typet type)

Definition at line 158 of file value_set_analysis_fi.cpp.

◆ get_entries()

void value_set_analysis_fit::get_entries ( const symbolt symbol,
std::list< value_set_fit::entryt > &  dest 

Definition at line 84 of file value_set_analysis_fi.cpp.

◆ get_entries_rec()

void value_set_analysis_fit::get_entries_rec ( const irep_idt identifier,
const std::string &  suffix,
const typet type,
std::list< value_set_fit::entryt > &  dest 

Definition at line 91 of file value_set_analysis_fi.cpp.

◆ get_globals()

void value_set_analysis_fit::get_globals ( std::list< value_set_fit::entryt > &  dest)

Definition at line 145 of file value_set_analysis_fi.cpp.

◆ get_values()

void value_set_analysis_fit::get_values ( const irep_idt function_id,
locationt  l,
const exprt expr,
std::list< exprt > &  dest 

Implements value_setst.

Definition at line 61 of file value_set_analysis_fi.h.

◆ initialize() [1/2]

void value_set_analysis_fit::initialize ( const goto_programt goto_program)

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 22 of file value_set_analysis_fi.cpp.

◆ initialize() [2/2]

void value_set_analysis_fit::initialize ( const goto_functionst goto_functions)

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 29 of file value_set_analysis_fi.cpp.

Member Data Documentation

◆ track_options

track_optionst value_set_analysis_fit::track_options

Definition at line 42 of file value_set_analysis_fi.h.

The documentation for this class was generated from the following files: