CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
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

 
 
- Public Types inherited from value_setst
typedef std::list< exprtvaluest
 
 
- Public Types inherited from flow_insensitive_analysis_baset
 
 

Public Member Functions

 
 
 
std::vector< exprtget_values (const irep_idt &function_id, locationt l, const exprt &expr) override
 
- Public Member Functions inherited from value_setst
 
 
- Public Member Functions inherited from flow_insensitive_analysist< value_set_domain_fit >
 
 
 
 
- Public Member Functions inherited from flow_insensitive_analysis_baset
 
 
 
virtual void  update (const goto_functionst &goto_functions)
 
virtual void  operator() (const irep_idt &function_id, const goto_programt &goto_program)
 
 
 
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

 
void  get_globals (std::list< value_set_fit::entryt > &dest)
 
void  add_vars (const goto_functionst &goto_functions)
 
 
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 >
 
 
 
- Protected Member Functions inherited from flow_insensitive_analysis_baset
 
 
bool  fixedpoint (const irep_idt &function_id, const goto_programt &goto_program, 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

 
- Protected Attributes inherited from flow_insensitive_analysist< value_set_domain_fit >
 
- Protected Attributes inherited from flow_insensitive_analysis_baset
 
 
 
 

Additional Inherited Members

- Public Attributes inherited from flow_insensitive_analysis_baset
 
 
- Protected Types inherited from flow_insensitive_analysis_baset
typedef std::priority_queue< locationt, std::vector< locationt >, goto_programt::target_less_thanworking_sett
 
 
 
 
- Static Protected Member Functions inherited from flow_insensitive_analysis_baset
 

Detailed Description

Definition at line 22 of file value_set_analysis_fi.h.

Member Typedef Documentation

◆  baset

Definition at line 38 of file value_set_analysis_fi.h.

Member Enumeration Documentation

◆  track_optionst

Enumerator
TRACK_ALL_POINTERS 
TRACK_FUNCTION_POINTERS 

Definition at line 27 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  
)
inline

Definition at line 30 of file value_set_analysis_fi.h.

Member Function Documentation

◆  add_vars() [1/2]

void value_set_analysis_fit::add_vars ( const goto_functionstgoto_functions )
protected

Definition at line 125 of file value_set_analysis_fi.cpp.

◆  add_vars() [2/2]

void value_set_analysis_fit::add_vars ( const goto_programtgoto_programa )
protected

Definition at line 34 of file value_set_analysis_fi.cpp.

◆  check_type()

bool value_set_analysis_fit::check_type ( const typettype )
protected

Definition at line 165 of file value_set_analysis_fi.cpp.

◆  get_entries()

void value_set_analysis_fit::get_entries ( const symboltsymbol,
std::list< value_set_fit::entryt > &  dest 
)
protected

Definition at line 82 of file value_set_analysis_fi.cpp.

◆  get_entries_rec()

void value_set_analysis_fit::get_entries_rec ( const irep_idtidentifier,
const std::string &  suffix,
const typettype,
std::list< value_set_fit::entryt > &  dest 
)
protected

Definition at line 89 of file value_set_analysis_fi.cpp.

◆  get_globals()

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

Definition at line 152 of file value_set_analysis_fi.cpp.

◆  get_values()

std::vector< exprt > value_set_analysis_fit::get_values ( const irep_idtfunction_id,
const exprtexpr 
)
overridevirtual

Implements value_setst.

Definition at line 209 of file value_set_analysis_fi.cpp.

◆  initialize() [1/2]

void value_set_analysis_fit::initialize ( const goto_functionstgoto_functions )
overridevirtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 27 of file value_set_analysis_fi.cpp.

◆  initialize() [2/2]

void value_set_analysis_fit::initialize ( const goto_programtgoto_program )
overridevirtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 20 of file value_set_analysis_fi.cpp.

Member Data Documentation

◆  track_options

track_optionst value_set_analysis_fit::track_options
protected

Definition at line 44 of file value_set_analysis_fi.h.


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

AltStyle によって変換されたページ (->オリジナル) /