cprover
uncaught_exceptions_domaint Class Reference

#include <uncaught_exceptions_analysis.h>

Collaboration diagram for uncaught_exceptions_domaint:
[legend]

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_idtthrown
 
class_hierarchyt class_hierarchy
 

Detailed Description

Definition at line 24 of file uncaught_exceptions_analysis.h.

Member Typedef Documentation

◆ stack_caughtt

typedef std::vector<std::set<irep_idt> > uncaught_exceptions_domaint::stack_caughtt
private

Definition at line 50 of file uncaught_exceptions_analysis.h.

Member Function Documentation

◆ get_elements()

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().

◆ get_exception_symbol()

exprt uncaught_exceptions_domaint::get_exception_symbol ( const exprt exor)
static

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().

◆ get_exception_type()

irep_idt uncaught_exceptions_domaint::get_exception_type ( const typet type)
static

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().

◆ join() [1/3]

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().

◆ join() [2/3]

void uncaught_exceptions_domaint::join ( const std::set< irep_idt > &  elements)

Definition at line 45 of file uncaught_exceptions_analysis.cpp.

References thrown.

◆ join() [3/3]

void uncaught_exceptions_domaint::join ( const std::vector< irep_idt > &  elements)

Definition at line 51 of file uncaught_exceptions_analysis.cpp.

References thrown.

◆ make_top()

void uncaught_exceptions_domaint::make_top ( )
inline

◆ operator()()

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().

◆ transform()

Member Data Documentation

◆ class_hierarchy

class_hierarchyt uncaught_exceptions_domaint::class_hierarchy
private

Definition at line 53 of file uncaught_exceptions_analysis.h.

Referenced by operator()(), and transform().

◆ stack_caught

stack_caughtt uncaught_exceptions_domaint::stack_caught
private

Definition at line 51 of file uncaught_exceptions_analysis.h.

Referenced by make_top(), and transform().

◆ thrown

std::set<irep_idt> uncaught_exceptions_domaint::thrown
private

Definition at line 52 of file uncaught_exceptions_analysis.h.

Referenced by get_elements(), join(), make_top(), and transform().


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