CBMC
|
computes in exceptions_map an overapproximation of the exceptions thrown by each method More...
#include <uncaught_exceptions_analysis.h>
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 178 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 241 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 213 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.