Loading...

Searching...

No Matches

flow_insensitive_analysis_baset Class Referenceabstract

#include <flow_insensitive_analysis.h>

+ Inheritance diagram for flow_insensitive_analysis_baset:

[フレーム]

[legend]

+ Collaboration diagram for flow_insensitive_analysis_baset:

[フレーム]

[legend]

Public Types

typedef flow_insensitive_abstract_domain_baset statet

typedef goto_programt::const_targett locationt

Public Member Functions

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 clear ()

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)

Public Attributes

std::set< locationt, goto_programt::target_less_than > seen_locations

std::map< locationt, unsigned, goto_programt::target_less_than > statistics

Protected Types

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

Protected Member Functions

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)

virtual statet & get_state ()=0

virtual const statet & get_state () const =0

virtual void get_reference_set (const exprt &expr, expr_sett &expr_set)=0

Static Protected Member Functions

static locationt successor (locationt l)

Protected Attributes

const namespacet & ns

functions_donet functions_done

recursion_sett recursion_set

bool initialized

Detailed Description

Definition at line 90 of file flow_insensitive_analysis.h.

Member Typedef Documentation

◆ expr_sett

typedef flow_insensitive_abstract_domain_baset::expr_sett flow_insensitive_analysis_baset::expr_sett

protected

Definition at line 226 of file flow_insensitive_analysis.h.

◆ functions_donet

typedef std::set<irep_idt> flow_insensitive_analysis_baset::functions_donet

protected

Definition at line 196 of file flow_insensitive_analysis.h.

◆ locationt

typedef goto_programt::const_targett flow_insensitive_analysis_baset::locationt

Definition at line 94 of file flow_insensitive_analysis.h.

◆ recursion_sett

typedef std::set<irep_idt> flow_insensitive_analysis_baset::recursion_sett

protected

Definition at line 199 of file flow_insensitive_analysis.h.

◆ statet

typedef flow_insensitive_abstract_domain_baset flow_insensitive_analysis_baset::statet

Definition at line 93 of file flow_insensitive_analysis.h.

◆ working_sett

typedef std::priority_queue< locationt, std::vector<locationt>, goto_programt::target_less_than> flow_insensitive_analysis_baset::working_sett

protected

Definition at line 162 of file flow_insensitive_analysis.h.

Constructor & Destructor Documentation

◆ flow_insensitive_analysis_baset()

flow_insensitive_analysis_baset::flow_insensitive_analysis_baset ( const namespacet & _ns )

inlineexplicit

Definition at line 105 of file flow_insensitive_analysis.h.

◆ ~flow_insensitive_analysis_baset()

virtual flow_insensitive_analysis_baset::~flow_insensitive_analysis_baset ( )

inlinevirtual

Definition at line 137 of file flow_insensitive_analysis.h.

Member Function Documentation

◆ clear()

virtual void flow_insensitive_analysis_baset::clear ( )

inlinevirtual

Reimplemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

Definition at line 141 of file flow_insensitive_analysis.h.

◆ do_function_call()

bool flow_insensitive_analysis_baset::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

Definition at line 190 of file flow_insensitive_analysis.cpp.

◆ do_function_call_rec()

bool flow_insensitive_analysis_baset::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

)

protected

Definition at line 273 of file flow_insensitive_analysis.cpp.

◆ fixedpoint() [1/2]

void flow_insensitive_analysis_baset::fixedpoint ( const goto_functionst & goto_functions )

protected

Definition at line 379 of file flow_insensitive_analysis.cpp.

◆ fixedpoint() [2/2]

bool flow_insensitive_analysis_baset::fixedpoint ( const irep_idt & function_id,

const goto_programt & goto_program,

const goto_functionst & goto_functions

)

protected

Definition at line 96 of file flow_insensitive_analysis.cpp.

◆ get_next()

flow_insensitive_analysis_baset::locationt flow_insensitive_analysis_baset::get_next ( working_sett & working_set )

protected

Definition at line 80 of file flow_insensitive_analysis.cpp.

◆ get_reference_set()

virtual void flow_insensitive_analysis_baset::get_reference_set ( const exprt & expr,

expr_sett & expr_set

)

protectedpure virtual

Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

◆ get_state() [1/2]

virtual const statet & flow_insensitive_analysis_baset::get_state ( ) const

protectedpure virtual

Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

◆ get_state() [2/2]

virtual statet & flow_insensitive_analysis_baset::get_state ( )

protectedpure virtual

Implemented in flow_insensitive_analysist< T >, and flow_insensitive_analysist< value_set_domain_fit >.

◆ initialize() [1/2]

virtual void flow_insensitive_analysis_baset::initialize ( const goto_functionst & )

inlinevirtual

Reimplemented in value_set_analysis_fit.

Definition at line 119 of file flow_insensitive_analysis.h.

◆ initialize() [2/2]

virtual void flow_insensitive_analysis_baset::initialize ( const goto_programt & )

inlinevirtual

Reimplemented in value_set_analysis_fit.

Definition at line 111 of file flow_insensitive_analysis.h.

◆ operator()() [1/2]

void flow_insensitive_analysis_baset::operator() ( const goto_functionst & goto_functions )

virtual

Definition at line 43 of file flow_insensitive_analysis.cpp.

◆ operator()() [2/2]

void flow_insensitive_analysis_baset::operator() ( const irep_idt & function_id,

const goto_programt & goto_program

)

virtual

Definition at line 50 of file flow_insensitive_analysis.cpp.

◆ output() [1/2]

void flow_insensitive_analysis_baset::output ( const goto_functionst & goto_functions,

std::ostream & out

)

virtual

Definition at line 58 of file flow_insensitive_analysis.cpp.

◆ output() [2/2]

void flow_insensitive_analysis_baset::output ( const irep_idt & function_id,

const goto_programt & goto_program,

std::ostream & out

)

virtual

Definition at line 71 of file flow_insensitive_analysis.cpp.

◆ put_in_working_set()

void flow_insensitive_analysis_baset::put_in_working_set ( working_sett & working_set,

locationt l

)

inlineprotected

Definition at line 166 of file flow_insensitive_analysis.h.

◆ seen()

bool flow_insensitive_analysis_baset::seen ( const locationt & l )

inline

Definition at line 100 of file flow_insensitive_analysis.h.

◆ successor()

static locationt flow_insensitive_analysis_baset::successor ( locationt l )

inlinestaticprotected

Definition at line 190 of file flow_insensitive_analysis.h.

◆ update() [1/2]

void flow_insensitive_analysis_baset::update ( const goto_functionst & goto_functions )

virtual

Definition at line 394 of file flow_insensitive_analysis.cpp.

◆ update() [2/2]

void flow_insensitive_analysis_baset::update ( const goto_programt & goto_program )

virtual

Definition at line 399 of file flow_insensitive_analysis.cpp.

◆ visit()

bool flow_insensitive_analysis_baset::visit ( const irep_idt & function_id,

locationt l,

working_sett & working_set,

const goto_programt & goto_program,

const goto_functionst & goto_functions

)

protected

Definition at line 125 of file flow_insensitive_analysis.cpp.

Member Data Documentation

◆ functions_done

functions_donet flow_insensitive_analysis_baset::functions_done

protected

Definition at line 197 of file flow_insensitive_analysis.h.

◆ initialized

bool flow_insensitive_analysis_baset::initialized

protected

Definition at line 202 of file flow_insensitive_analysis.h.

◆ ns

const namespacet& flow_insensitive_analysis_baset::ns

protected

Definition at line 156 of file flow_insensitive_analysis.h.

◆ recursion_set

recursion_sett flow_insensitive_analysis_baset::recursion_set

protected

Definition at line 200 of file flow_insensitive_analysis.h.

◆ seen_locations

std::set<locationt, goto_programt::target_less_than> flow_insensitive_analysis_baset::seen_locations

Definition at line 96 of file flow_insensitive_analysis.h.

◆ statistics

std::map<locationt, unsigned, goto_programt::target_less_than> flow_insensitive_analysis_baset::statistics

Definition at line 98 of file flow_insensitive_analysis.h.

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

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