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

Public Member Functions

 remove_exceptionst (symbol_tablet &_symbol_table)
 
void operator() (goto_functionst &goto_functions)
 

Protected Member Functions

void add_exceptional_returns (const goto_functionst::function_mapt::iterator &)
 adds exceptional return variables for every function that may escape exceptions More...
 
void instrument_exception_handler (const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &)
 at the beginning of each handler in function f adds exc=f::exception_value; f::exception_value=NULL; More...
 
void instrument_throw (const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, const stack_catcht &, std::vector< exprt > &)
 instruments each throw with conditional GOTOS to the corresponding exception handlers More...
 
void instrument_function_call (const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, const stack_catcht &, std::vector< exprt > &)
 instruments each function call that may escape exceptions with conditional GOTOS to the corresponding exception handlers More...
 
void instrument_exceptions (const goto_functionst::function_mapt::iterator &)
 instruments throws, function calls that may escape exceptions and exception handlers. More...
 

Protected Attributes

symbol_tabletsymbol_table
 

Private Types

typedef std::vector< std::pair< irep_idt, goto_programt::targett > > catch_handlerst
 
typedef std::vector< catch_handlerststack_catcht
 

Detailed Description

Definition at line 27 of file remove_exceptions.cpp.

Member Typedef Documentation

§ catch_handlerst

typedef std::vector<std::pair< irep_idt, goto_programt::targett> > remove_exceptionst::catch_handlerst
private

Definition at line 30 of file remove_exceptions.cpp.

§ stack_catcht

typedef std::vector<catch_handlerst> remove_exceptionst::stack_catcht
private

Definition at line 31 of file remove_exceptions.cpp.

Constructor & Destructor Documentation

§ remove_exceptionst()

remove_exceptionst::remove_exceptionst ( symbol_tablet _symbol_table)
inlineexplicit

Definition at line 34 of file remove_exceptions.cpp.

References operator()().

Member Function Documentation

§ add_exceptional_returns()

void remove_exceptionst::add_exceptional_returns ( const goto_functionst::function_mapt::iterator &  func_it)
protected

§ instrument_exception_handler()

void remove_exceptionst::instrument_exception_handler ( const goto_functionst::function_mapt::iterator &  func_it,
const goto_programt::instructionst::iterator &  instr_it 
)
protected

at the beginning of each handler in function f adds exc=f::exception_value; f::exception_value=NULL;

Definition at line 132 of file remove_exceptions.cpp.

References CATCH, EXC_SUFFIX, symbol_tablet::has_symbol(), id2string(), goto_program_templatet< codeT, guardT >::insert_after(), symbol_tablet::lookup(), exprt::op0(), pointer_type(), symbolt::symbol_expr(), symbol_table, and exprt::type().

Referenced by instrument_exceptions().

§ instrument_exceptions()

void remove_exceptionst::instrument_exceptions ( const goto_functionst::function_mapt::iterator &  func_it)
protected

instruments throws, function calls that may escape exceptions and exception handlers.

Additionally, it re-computes the live-range of local variables in order to add DEAD instructions.

Definition at line 354 of file remove_exceptions.cpp.

References CATCH, goto_program_templatet< codeT, guardT >::empty(), Forall_goto_program_instructions, FUNCTION_CALL, instrument_exception_handler(), instrument_function_call(), instrument_throw(), code_declt::symbol(), THROW, and to_code_decl().

Referenced by operator()().

§ instrument_function_call()

void remove_exceptionst::instrument_function_call ( const goto_functionst::function_mapt::iterator &  func_it,
const goto_programt::instructionst::iterator &  instr_it,
const stack_catcht stack_catch,
std::vector< exprt > &  locals 
)
protected

§ instrument_throw()

void remove_exceptionst::instrument_throw ( const goto_functionst::function_mapt::iterator &  func_it,
const goto_programt::instructionst::iterator &  instr_it,
const stack_catcht stack_catch,
std::vector< exprt > &  locals 
)
protected

§ operator()()

void remove_exceptionst::operator() ( goto_functionst goto_functions)

Member Data Documentation

§ symbol_table

symbol_tablet& remove_exceptionst::symbol_table
protected

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