cprover
const_function_pointer_propagationt Class Reference
Collaboration diagram for const_function_pointer_propagationt:
[legend]

Classes

class  arg_stackt
 

Public Member Functions

 const_function_pointer_propagationt (symbol_tablet &_symbol_table, goto_functionst &_goto_functions, messaget &_message)
 
void propagate ()
 

Protected Member Functions

bool resolve (const irep_idt &symb, symbol_exprt &goto_function, unsigned &stack_scope)
 
bool add (const irep_idt &symb, const symbol_exprt &goto_function)
 
bool add (const irep_idt &symb, const symbol_exprt &goto_function, unsigned scope)
 
bool remove (const irep_idt &symb)
 
bool has (const irep_idt &symb) const
 
symbol_exprt get (const irep_idt &symb)
 
void propagate (const irep_idt &function)
 
void dup_caller_and_inline_callee (const symbol_exprt &function, unsigned stack_scope)
 

Protected Attributes

symbol_tabletsymbol_table
 
goto_functionstgoto_functions
 
const namespacet ns
 
messagetmessage
 
std::unordered_map< irep_idt, unsigned, irep_id_hashmap_unique
 
std::unordered_map< irep_idt, symbol_exprt, irep_id_hashpointer_to_fun
 
std::unordered_map< irep_idt, unsigned, irep_id_hashpointer_to_stack
 
std::unordered_map< irep_idt, unsigned, irep_id_hashfun_id_to_invok
 
goto_programt::const_targetst callsite_stack
 
std::set< irep_idtfunctions_met
 

Detailed Description

Definition at line 28 of file propagate_const_function_pointers.cpp.

Constructor & Destructor Documentation

§ const_function_pointer_propagationt()

const_function_pointer_propagationt::const_function_pointer_propagationt ( symbol_tablet _symbol_table,
goto_functionst _goto_functions,
messaget _message 
)
inline

Definition at line 132 of file propagate_const_function_pointers.cpp.

Member Function Documentation

§ add() [1/2]

bool const_function_pointer_propagationt::add ( const irep_idt symb,
const symbol_exprt goto_function 
)
inlineprotected

§ add() [2/2]

bool const_function_pointer_propagationt::add ( const irep_idt symb,
const symbol_exprt goto_function,
unsigned  scope 
)
inlineprotected

§ dup_caller_and_inline_callee()

§ get()

symbol_exprt const_function_pointer_propagationt::get ( const irep_idt symb)
inlineprotected

§ has()

bool const_function_pointer_propagationt::has ( const irep_idt symb) const
inlineprotected

§ propagate() [1/2]

§ propagate() [2/2]

void const_function_pointer_propagationt::propagate ( )
inline

§ remove()

bool const_function_pointer_propagationt::remove ( const irep_idt symb)
inlineprotected

§ resolve()

bool const_function_pointer_propagationt::resolve ( const irep_idt symb,
symbol_exprt goto_function,
unsigned &  stack_scope 
)
inlineprotected

Definition at line 50 of file propagate_const_function_pointers.cpp.

References messaget::debug(), and messaget::eom().

Referenced by propagate().

Member Data Documentation

§ callsite_stack

goto_programt::const_targetst const_function_pointer_propagationt::callsite_stack
protected

§ fun_id_to_invok

std::unordered_map<irep_idt, unsigned, irep_id_hash> const_function_pointer_propagationt::fun_id_to_invok
protected

§ functions_met

std::set<irep_idt> const_function_pointer_propagationt::functions_met
protected

Definition at line 109 of file propagate_const_function_pointers.cpp.

Referenced by propagate().

§ goto_functions

goto_functionst& const_function_pointer_propagationt::goto_functions
protected

§ map_unique

std::unordered_map<irep_idt, unsigned, irep_id_hash> const_function_pointer_propagationt::map_unique
protected

Definition at line 36 of file propagate_const_function_pointers.cpp.

Referenced by dup_caller_and_inline_callee().

§ message

§ ns

const namespacet const_function_pointer_propagationt::ns
protected

Definition at line 33 of file propagate_const_function_pointers.cpp.

Referenced by dup_caller_and_inline_callee().

§ pointer_to_fun

std::unordered_map<irep_idt, symbol_exprt, irep_id_hash> const_function_pointer_propagationt::pointer_to_fun
protected

Definition at line 39 of file propagate_const_function_pointers.cpp.

Referenced by dup_caller_and_inline_callee().

§ pointer_to_stack

std::unordered_map<irep_idt, unsigned, irep_id_hash> const_function_pointer_propagationt::pointer_to_stack
protected

Definition at line 42 of file propagate_const_function_pointers.cpp.

§ symbol_table

symbol_tablet& const_function_pointer_propagationt::symbol_table
protected

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