cprover
|
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_tablet & | symbol_table |
Private Types | |
typedef std::vector< std::pair< irep_idt, goto_programt::targett > > | catch_handlerst |
typedef std::vector< catch_handlerst > | stack_catcht |
Definition at line 27 of file remove_exceptions.cpp.
|
private |
Definition at line 30 of file remove_exceptions.cpp.
|
private |
Definition at line 31 of file remove_exceptions.cpp.
|
inlineexplicit |
Definition at line 34 of file remove_exceptions.cpp.
|
protected |
adds exceptional return variables for every function that may escape exceptions
Definition at line 70 of file remove_exceptions.cpp.
References symbol_tablet::add(), goto_program_templatet< codeT, guardT >::empty(), EXC_SUFFIX, forall_goto_program_instructions, symbol_tablet::has_symbol(), id2string(), goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::instructions, symbolt::is_static_lifetime, symbol_tablet::lookup(), pointer_type(), symbol_table, and symbol_tablet::symbols.
Referenced by operator()().
|
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().
|
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()().
|
protected |
instruments each function call that may escape exceptions with conditional GOTOS to the corresponding exception handlers
Definition at line 257 of file remove_exceptions.cpp.
References EXC_SUFFIX, code_function_callt::function(), FUNCTION_CALL, goto_program_templatet< codeT, guardT >::get_end_function(), symbol_tablet::has_symbol(), irept::id(), id2string(), goto_program_templatet< codeT, guardT >::insert_after(), symbol_tablet::lookup(), pointer_type(), symbolt::symbol_expr(), symbol_table, to_code_function_call(), and to_symbol_expr().
Referenced by instrument_exceptions().
|
protected |
instruments each throw with conditional GOTOS to the corresponding exception handlers
Definition at line 177 of file remove_exceptions.cpp.
References ASSIGN, EXC_SUFFIX, goto_program_templatet< codeT, guardT >::get_end_function(), exprt::has_operands(), irept::id(), id2string(), goto_program_templatet< codeT, guardT >::insert_after(), symbol_tablet::lookup(), exprt::op0(), symbolt::symbol_expr(), symbol_table, THROW, and exprt::type().
Referenced by instrument_exceptions().
void remove_exceptionst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 436 of file remove_exceptions.cpp.
References add_exceptional_returns(), Forall_goto_functions, and instrument_exceptions().
|
protected |
Definition at line 43 of file remove_exceptions.cpp.
Referenced by add_exceptional_returns(), instrument_exception_handler(), instrument_function_call(), and instrument_throw().