CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Public Attributes | Protected Types | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
flow_insensitive_analysis_baset Class Referenceabstract

#include <flow_insensitive_analysis.h>

+ Inheritance diagram for flow_insensitive_analysis_baset:
+ Collaboration diagram for flow_insensitive_analysis_baset:

Public Types

 
 

Public Member Functions

 
 
 
 
 
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)
 

Public Attributes

 
 

Protected Types

typedef std::priority_queue< locationt, std::vector< locationt >, goto_programt::target_less_thanworking_sett
 
 
 
 

Protected Member Functions

 
 
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)
 
 
 
 

Static Protected Member Functions

 

Protected Attributes

 
 
 
 

Detailed Description

Definition at line 90 of file flow_insensitive_analysis.h.

Member Typedef Documentation

◆  expr_sett

Definition at line 226 of file flow_insensitive_analysis.h.

◆  functions_donet

Definition at line 196 of file flow_insensitive_analysis.h.

◆  locationt

Definition at line 94 of file flow_insensitive_analysis.h.

◆  recursion_sett

Definition at line 199 of file flow_insensitive_analysis.h.

◆  statet

Definition at line 93 of file flow_insensitive_analysis.h.

◆  working_sett

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_idtcalling_function,
locationt  l_call,
const goto_functionstgoto_functions,
const goto_functionst::function_mapt::const_iterator  f_it,
const exprt::operandstarguments,
statetnew_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_idtcalling_function,
locationt  l_call,
const exprtfunction,
const exprt::operandstarguments,
statetnew_state,
const goto_functionstgoto_functions 
)
protected

Definition at line 273 of file flow_insensitive_analysis.cpp.

◆  fixedpoint() [1/2]

void flow_insensitive_analysis_baset::fixedpoint ( const goto_functionstgoto_functions )
protected

Definition at line 379 of file flow_insensitive_analysis.cpp.

◆  fixedpoint() [2/2]

bool flow_insensitive_analysis_baset::fixedpoint ( const irep_idtfunction_id,
const goto_programtgoto_program,
const goto_functionstgoto_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_settworking_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 exprtexpr,
expr_settexpr_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_functionstgoto_functions )
virtual

Definition at line 43 of file flow_insensitive_analysis.cpp.

◆  operator()() [2/2]

void flow_insensitive_analysis_baset::operator() ( const irep_idtfunction_id,
const goto_programtgoto_program 
)
virtual

Definition at line 50 of file flow_insensitive_analysis.cpp.

◆  output() [1/2]

void flow_insensitive_analysis_baset::output ( const goto_functionstgoto_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_idtfunction_id,
const goto_programtgoto_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_settworking_set,
locationt  l 
)
inlineprotected

Definition at line 166 of file flow_insensitive_analysis.h.

◆  seen()

bool flow_insensitive_analysis_baset::seen ( const locationtl )
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_functionstgoto_functions )
virtual

Definition at line 394 of file flow_insensitive_analysis.cpp.

◆  update() [2/2]

void flow_insensitive_analysis_baset::update ( const goto_programtgoto_program )
virtual

Definition at line 399 of file flow_insensitive_analysis.cpp.

◆  visit()

bool flow_insensitive_analysis_baset::visit ( const irep_idtfunction_id,
locationt  l,
working_settworking_set,
const goto_programtgoto_program,
const goto_functionstgoto_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:

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