cprover
value_set_analysis_fivrnst Class Reference

#include <value_set_analysis_fivrns.h>

+ Inheritance diagram for value_set_analysis_fivrnst:
+ Collaboration diagram for value_set_analysis_fivrnst:

Public Types

enum  track_optionst { TRACK_ALL_POINTERS, TRACK_FUNCTION_POINTERS }
 
typedef flow_insensitive_analysist< value_set_domain_fivrnstbaset
 
- Public Types inherited from value_setst
typedef std::list< exprtvaluest
 
- Public Types inherited from flow_insensitive_analysist< value_set_domain_fivrnst >
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_fivrnst (const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
 
virtual void initialize (const goto_programt &goto_program)
 
virtual void initialize (const goto_functionst &goto_functions)
 
virtual void output (locationt l, std::ostream &out)
 
void output (const goto_programt &goto_program, std::ostream &out)
 
virtual void get_values (locationt l, const exprt &expr, std::list< exprt > &dest)
 
- Public Member Functions inherited from value_setst
 value_setst ()
 
virtual ~value_setst ()
 
- Public Member Functions inherited from flow_insensitive_analysist< value_set_domain_fivrnst >
 flow_insensitive_analysist (const namespacet &_ns)
 
virtual void clear ()
 
value_set_domain_fivrnstget_data ()
 
const value_set_domain_fivrnstget_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 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)
 

Protected Member Functions

bool check_type (const typet &type)
 
void get_globals (std::list< value_set_fivrnst::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_fivrnst::entryt > &dest)
 
void get_entries_rec (const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrnst::entryt > &dest)
 
- Protected Member Functions inherited from flow_insensitive_analysist< value_set_domain_fivrnst >
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
virtual void output (const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const
 
locationt get_next (working_sett &working_set)
 
void put_in_working_set (working_sett &working_set, locationt l)
 
bool fixedpoint (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 (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
 
bool do_function_call_rec (locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
 
bool do_function_call (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_fivrnst >
value_set_domain_fivrnst 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 21 of file value_set_analysis_fivrns.h.

Member Typedef Documentation

◆ baset

Member Enumeration Documentation

◆ track_optionst

Enumerator
TRACK_ALL_POINTERS 
TRACK_FUNCTION_POINTERS 

Definition at line 26 of file value_set_analysis_fivrns.h.

Constructor & Destructor Documentation

◆ value_set_analysis_fivrnst()

value_set_analysis_fivrnst::value_set_analysis_fivrnst ( const namespacet _ns,
track_optionst  _track_options = TRACK_ALL_POINTERS 
)
inline

Definition at line 29 of file value_set_analysis_fivrns.h.

Member Function Documentation

◆ add_vars() [1/2]

void value_set_analysis_fivrnst::add_vars ( const goto_functionst goto_functions)
protected

Definition at line 108 of file value_set_analysis_fivrns.cpp.

◆ add_vars() [2/2]

void value_set_analysis_fivrnst::add_vars ( const goto_programt goto_programa)
protected

Definition at line 36 of file value_set_analysis_fivrns.cpp.

◆ check_type()

bool value_set_analysis_fivrnst::check_type ( const typet type)
protected

Definition at line 148 of file value_set_analysis_fivrns.cpp.

◆ get_entries()

void value_set_analysis_fivrnst::get_entries ( const symbolt symbol,
std::list< value_set_fivrnst::entryt > &  dest 
)
protected

Definition at line 74 of file value_set_analysis_fivrns.cpp.

◆ get_entries_rec()

void value_set_analysis_fivrnst::get_entries_rec ( const irep_idt identifier,
const std::string &  suffix,
const typet type,
std::list< value_set_fivrnst::entryt > &  dest 
)
protected

Definition at line 81 of file value_set_analysis_fivrns.cpp.

◆ get_globals()

void value_set_analysis_fivrnst::get_globals ( std::list< value_set_fivrnst::entryt > &  dest)
protected

Definition at line 135 of file value_set_analysis_fivrns.cpp.

◆ get_values()

virtual void value_set_analysis_fivrnst::get_values ( locationt  l,
const exprt expr,
std::list< exprt > &  dest 
)
inlinevirtual

Implements value_setst.

Definition at line 83 of file value_set_analysis_fivrns.h.

◆ initialize() [1/2]

void value_set_analysis_fivrnst::initialize ( const goto_programt goto_program)
virtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 22 of file value_set_analysis_fivrns.cpp.

◆ initialize() [2/2]

void value_set_analysis_fivrnst::initialize ( const goto_functionst goto_functions)
virtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 29 of file value_set_analysis_fivrns.cpp.

◆ output() [1/2]

virtual void value_set_analysis_fivrnst::output ( locationt  l,
std::ostream &  out 
)
inlinevirtual

Definition at line 44 of file value_set_analysis_fivrns.h.

◆ output() [2/2]

void value_set_analysis_fivrnst::output ( const goto_programt goto_program,
std::ostream &  out 
)
inlinevirtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 51 of file value_set_analysis_fivrns.h.

Member Data Documentation

◆ track_options

track_optionst value_set_analysis_fivrnst::track_options
protected

Definition at line 64 of file value_set_analysis_fivrns.h.


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