cprover
flow_insensitive_analysist< T > Class Template Reference

#include <flow_insensitive_analysis.h>

Inheritance diagram for flow_insensitive_analysist< T >:
[legend]
Collaboration diagram for flow_insensitive_analysist< T >:
[legend]

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 &goto_program)
 
virtual void initialize (const goto_functionst &goto_functions)
 
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)
 
virtual void output (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
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

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< 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

template<typename T>
class flow_insensitive_analysist< T >

Definition at line 226 of file flow_insensitive_analysis.h.

Member Typedef Documentation

§ locationt

Definition at line 235 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 230 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 237 of file flow_insensitive_analysis.h.

§ dummy()

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

Definition at line 262 of file flow_insensitive_analysis.h.

§ get_data() [1/2]

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

Definition at line 243 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 244 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 253 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 249 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 251 of file flow_insensitive_analysis.h.

Member Data Documentation

§ state

template<typename T>
T flow_insensitive_analysist< T >::state
protected

Definition at line 247 of file flow_insensitive_analysis.h.


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