CBMC
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

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

 flow_insensitive_analysist (const namespacet &_ns)
 
virtual void clear ()
 
T & get_data ()
 
const T & 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 initialize (const goto_programt &)
 
virtual void initialize (const goto_functionst &)
 
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

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)
 
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
const namespacetns
 
functions_donet functions_done
 
recursion_sett recursion_set
 
bool initialized
 

Private Member Functions

void dummy (const T &s)
 

Additional Inherited Members

- Public Attributes inherited from flow_insensitive_analysis_baset
std::set< locationt, goto_programt::target_less_thanseen_locations
 
std::map< locationt, unsigned, goto_programt::target_less_thanstatistics
 
- Protected Types inherited from flow_insensitive_analysis_baset
typedef std::priority_queue< locationt, std::vector< locationt >, goto_programt::target_less_thanworking_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

template<typename T>
class flow_insensitive_analysist< T >

Definition at line 235 of file flow_insensitive_analysis.h.

Member Typedef Documentation

◆ locationt

Definition at line 244 of file flow_insensitive_analysis.h.

Constructor & Destructor Documentation

◆ flow_insensitive_analysist()

template<typename T >
flow_insensitive_analysist< T >::flow_insensitive_analysist ( const namespacet _ns)
inlineexplicit

Definition at line 239 of file flow_insensitive_analysis.h.

Member Function Documentation

◆ clear()

template<typename T >
virtual void flow_insensitive_analysist< T >::clear ( void  )
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 exprt expr,
expr_sett expr_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 >
T flow_insensitive_analysist< T >::state
protected

Definition at line 256 of file flow_insensitive_analysis.h.


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