|
CBMC
|
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 |
computes in exceptions_map an overapproximation of the exceptions thrown by each method
Definition at line 62 of file uncaught_exceptions_analysis.h.
| typedef std::map<irep_idt, std::set<irep_idt> > uncaught_exceptions_analysist::exceptions_mapt |
Definition at line 65 of file uncaught_exceptions_analysis.h.
| 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 179 of file uncaught_exceptions_analysis.cpp.
| 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 242 of file uncaught_exceptions_analysis.cpp.
| 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 214 of file uncaught_exceptions_analysis.cpp.
|
friend |
Definition at line 78 of file uncaught_exceptions_analysis.h.
|
private |
Definition at line 81 of file uncaught_exceptions_analysis.h.
|
private |
Definition at line 82 of file uncaught_exceptions_analysis.h.