Loading...

Searching...

No Matches

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

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

T state

- Protected Attributes inherited from flow_insensitive_analysis_baset

const namespacet & ns

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

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 >

typedef goto_programt::const_targett flow_insensitive_analysist< T >::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 ( )

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:

/home/runner/work/cbmc/cbmc/src/analyses/flow_insensitive_analysis.h