cprover
|
#include <uncaught_exceptions_analysis.h>
Public Member Functions | |
void | transform (const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &) |
The transformer for the uncaught exceptions domain. More... | |
void | join (const irep_idt &) |
The join operator for the uncaught exceptions domain. More... | |
void | join (const std::set< irep_idt > &) |
void | join (const std::vector< irep_idt > &) |
void | make_top () |
const std::set< irep_idt > & | get_elements () const |
Returns the value of the private member thrown. More... | |
void | operator() (const namespacet &ns) |
Constructs the class hierarchy. More... | |
Static Public Member Functions | |
static irep_idt | get_exception_type (const typet &type) |
Returns the compile type of an exception. More... | |
static exprt | get_exception_symbol (const exprt &exor) |
Returns the symbol corresponding to an exception. More... | |
Private Types | |
typedef std::vector< std::set< irep_idt > > | stack_caughtt |
Private Attributes | |
stack_caughtt | stack_caught |
std::set< irep_idt > | thrown |
class_hierarchyt | class_hierarchy |
Definition at line 24 of file uncaught_exceptions_analysis.h.
|
private |
Definition at line 50 of file uncaught_exceptions_analysis.h.
const std::set< irep_idt > & uncaught_exceptions_domaint::get_elements | ( | ) | const |
Returns the value of the private member thrown.
Definition at line 135 of file uncaught_exceptions_analysis.cpp.
References thrown.
Referenced by uncaught_exceptions_analysist::collect_uncaught_exceptions().
Returns the symbol corresponding to an exception.
Definition at line 30 of file uncaught_exceptions_analysis.cpp.
References exprt::has_operands(), irept::id(), and exprt::op0().
Referenced by remove_exceptionst::instrument_throw(), and transform().
Returns the compile type of an exception.
Definition at line 18 of file uncaught_exceptions_analysis.cpp.
References irept::id(), PRECONDITION, typet::subtype(), and to_symbol_type().
Referenced by java_bytecode_convert_methodt::convert_athrow(), and transform().
void uncaught_exceptions_domaint::join | ( | const irep_idt & | element | ) |
The join operator for the uncaught exceptions domain.
Definition at line 39 of file uncaught_exceptions_analysis.cpp.
References thrown.
Referenced by transform().
void uncaught_exceptions_domaint::join | ( | const std::set< irep_idt > & | elements | ) |
Definition at line 45 of file uncaught_exceptions_analysis.cpp.
References thrown.
void uncaught_exceptions_domaint::join | ( | const std::vector< irep_idt > & | elements | ) |
Definition at line 51 of file uncaught_exceptions_analysis.cpp.
References thrown.
|
inline |
Definition at line 35 of file uncaught_exceptions_analysis.h.
References stack_caught, and thrown.
Referenced by uncaught_exceptions_analysist::collect_uncaught_exceptions().
void uncaught_exceptions_domaint::operator() | ( | const namespacet & | ns | ) |
Constructs the class hierarchy.
Definition at line 141 of file uncaught_exceptions_analysis.cpp.
References class_hierarchy, and namespacet::get_symbol_table().
void uncaught_exceptions_domaint::transform | ( | const goto_programt::const_targett | from, |
uncaught_exceptions_analysist & | uea, | ||
const namespacet & | |||
) |
The transformer for the uncaught exceptions domain.
Definition at line 59 of file uncaught_exceptions_analysis.cpp.
References CATCH, class_hierarchy, goto_programt::instructiont::code, DATA_INVARIANT, uncaught_exceptions_analysist::exceptions_map, irept::find(), code_function_callt::function(), FUNCTION_CALL, class_hierarchyt::get_children_trans(), get_exception_symbol(), get_exception_type(), symbol_exprt::get_identifier(), irept::get_sub(), exprt::has_operands(), irept::id(), join(), stack_caught, goto_programt::instructiont::targets, THROW, thrown, to_code_function_call(), to_symbol_expr(), exprt::type(), and goto_programt::instructiont::type.
Referenced by uncaught_exceptions_analysist::collect_uncaught_exceptions().
|
private |
Definition at line 53 of file uncaught_exceptions_analysis.h.
Referenced by operator()(), and transform().
|
private |
Definition at line 51 of file uncaught_exceptions_analysis.h.
Referenced by make_top(), and transform().
|
private |
Definition at line 52 of file uncaught_exceptions_analysis.h.
Referenced by get_elements(), join(), make_top(), and transform().