CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | Private Member Functions | List of all members
flow_insensitive_analysist< T > Class Template Reference

#include <flow_insensitive_analysis.h>

+ Inheritance diagram for flow_insensitive_analysist< T >:
+ Collaboration diagram for flow_insensitive_analysist< T >:

Public Types

 
- Public Types inherited from flow_insensitive_analysis_baset
 
 

Public Member Functions

 
 
T &  get_data ()
 
const T &  get_data () const
 
- 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

 
 
 
- 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

state
 
- Protected Attributes inherited from flow_insensitive_analysis_baset
 
 
 
 

Private Member Functions

void  dummy (const T &s)
 

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

template<typename T>
class flow_insensitive_analysist< T >

Definition at line 235 of file flow_insensitive_analysis.h.

Member Typedef Documentation

◆  locationt

template<typename T >

Definition at line 244 of file flow_insensitive_analysis.h.

Constructor & Destructor Documentation

◆  flow_insensitive_analysist()

template<typename T >

Definition at line 239 of file flow_insensitive_analysis.h.

Member Function Documentation

◆  clear()

template<typename T >
inlinevirtual

Reimplemented from flow_insensitive_analysis_baset.

Definition at line 246 of file flow_insensitive_analysis.h.

◆  dummy()

template<typename T >
void flow_insensitive_analysist< T >::dummy ( const T &  s )
inlineprivate

Definition at line 271 of file flow_insensitive_analysis.h.

◆  get_data() [1/2]

template<typename T >
T & flow_insensitive_analysist< T >::get_data ( )
inline

Definition at line 252 of file flow_insensitive_analysis.h.

◆  get_data() [2/2]

template<typename T >
const T & flow_insensitive_analysist< T >::get_data ( ) const
inline

Definition at line 253 of file flow_insensitive_analysis.h.

◆  get_reference_set()

template<typename T >
void flow_insensitive_analysist< T >::get_reference_set ( const exprtexpr,
expr_settexpr_set 
)
inlineprotectedvirtual

Implements flow_insensitive_analysis_baset.

Definition at line 262 of file flow_insensitive_analysis.h.

◆  get_state() [1/2]

template<typename T >
virtual statet & flow_insensitive_analysist< T >::get_state ( )
inlineprotectedvirtual

Implements flow_insensitive_analysis_baset.

Definition at line 258 of file flow_insensitive_analysis.h.

◆  get_state() [2/2]

template<typename T >
virtual const statet & flow_insensitive_analysist< T >::get_state ( ) const
inlineprotectedvirtual

Implements flow_insensitive_analysis_baset.

Definition at line 260 of file flow_insensitive_analysis.h.

Member Data Documentation

◆  state

template<typename T >
protected

Definition at line 256 of file flow_insensitive_analysis.h.


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

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