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:
[フレーム]
[legend]
+ Collaboration diagram for value_set_analysis_fit:
[フレーム]
[legend]

Public Types

enum   track_optionst { TRACK_ALL_POINTERS , TRACK_FUNCTION_POINTERS }
 
typedef flow_insensitive_analysist< value_set_domain_fit >  baset
 
- Public Types inherited from value_setst
typedef std::list< exprt >  valuest
 
- 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
 
std::vector< exprt >  get_values (const irep_idt &function_id, locationt l, const exprt &expr) 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_fit &  get_data ()
 
const value_set_domain_fit &  get_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 statet &  get_state ()
 
virtual const statet &  get_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)
 
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 namespacet &  ns
 
functions_donet  functions_done
 
recursion_sett  recursion_set
 
bool  initialized
 

Additional Inherited Members

- Public Attributes inherited from flow_insensitive_analysis_baset
std::set< locationt, goto_programt::target_less_than >  seen_locations
 
std::map< locationt, unsigned, goto_programt::target_less_than >  statistics
 
- Protected Types inherited from flow_insensitive_analysis_baset
typedef std::priority_queue< locationt, std::vector< locationt >, goto_programt::target_less_than >  working_sett
 
typedef std::set< irep_idt >  functions_donet
 
typedef std::set< irep_idt >  recursion_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 22 of file value_set_analysis_fi.h.

Member Typedef Documentation

◆  baset

typedef flow_insensitive_analysist<value_set_domain_fit> value_set_analysis_fit::baset

Definition at line 38 of file value_set_analysis_fi.h.

Member Enumeration Documentation

◆  track_optionst

enum value_set_analysis_fit::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_functionst &  goto_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_programt &  goto_programa )
protected

Definition at line 34 of file value_set_analysis_fi.cpp.

◆  check_type()

bool value_set_analysis_fit::check_type ( const typet &  type )
protected

Definition at line 165 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 
)
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_idt &  identifier,
const std::string &  suffix,
const typet &  type,
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_idt &  function_id,
flow_insensitive_analysis_baset::locationt  l,
const exprt &  expr 
)
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_functionst &  goto_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_programt &  goto_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 によって変換されたページ (->オリジナル) /