CBMC
uncaught_exceptions_analysist Class Reference

computes in exceptions_map an overapproximation of the exceptions thrown by each method More...

#include <uncaught_exceptions_analysis.h>

+ Collaboration diagram for uncaught_exceptions_analysist:

Public Types

typedef std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
 

Public Member Functions

void collect_uncaught_exceptions (const goto_functionst &, const namespacet &)
 Runs the uncaught exceptions analysis, which populates the exceptions map. More...
 
void output (const goto_functionst &) const
 Prints the exceptions map that maps each method to the set of exceptions that may escape it. More...
 
void operator() (const goto_functionst &, const namespacet &, exceptions_mapt &)
 Applies the uncaught exceptions analysis and outputs the result. More...
 

Private Attributes

uncaught_exceptions_domaint domain
 
exceptions_mapt exceptions_map
 

Friends

class uncaught_exceptions_domaint
 

Detailed Description

computes in exceptions_map an overapproximation of the exceptions thrown by each method

Definition at line 62 of file uncaught_exceptions_analysis.h.

Member Typedef Documentation

◆ exceptions_mapt

Definition at line 65 of file uncaught_exceptions_analysis.h.

Member Function Documentation

◆ collect_uncaught_exceptions()

void uncaught_exceptions_analysist::collect_uncaught_exceptions ( const goto_functionst goto_functions,
const namespacet ns 
)

Runs the uncaught exceptions analysis, which populates the exceptions map.

Definition at line 178 of file uncaught_exceptions_analysis.cpp.

◆ operator()()

void uncaught_exceptions_analysist::operator() ( const goto_functionst goto_functions,
const namespacet ns,
exceptions_mapt exceptions 
)

Applies the uncaught exceptions analysis and outputs the result.

Definition at line 241 of file uncaught_exceptions_analysis.cpp.

◆ output()

void uncaught_exceptions_analysist::output ( const goto_functionst goto_functions) const

Prints the exceptions map that maps each method to the set of exceptions that may escape it.

Definition at line 213 of file uncaught_exceptions_analysis.cpp.

Friends And Related Function Documentation

◆ uncaught_exceptions_domaint

friend class uncaught_exceptions_domaint
friend

Definition at line 78 of file uncaught_exceptions_analysis.h.

Member Data Documentation

◆ domain

uncaught_exceptions_domaint uncaught_exceptions_analysist::domain
private

Definition at line 81 of file uncaught_exceptions_analysis.h.

◆ exceptions_map

exceptions_mapt uncaught_exceptions_analysist::exceptions_map
private

Definition at line 82 of file uncaught_exceptions_analysis.h.


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