cprover
uncaught_exceptions_analysis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Over-approximative uncaught exceptions analysis
4 
5 Author: Cristina David
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H
13 #define CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H
14 
15 #include <map>
16 #include <set>
17 
20 
21 class goto_functionst;
22 class namespacet;
23 
26 
28 {
29  public:
32  const namespacet &);
33 
34  void join(const irep_idt &);
35  void join(const std::set<irep_idt> &);
36  void join(const std::vector<irep_idt> &);
37 
38  void make_top()
39  {
40  thrown.clear();
41  stack_caught.clear();
42  }
43 
44  static irep_idt get_exception_type(const typet &type);
45 
46  static exprt get_exception_symbol(const exprt &exor);
47 
48  const std::set<irep_idt> &get_elements() const;
49 
50  void operator()(const namespacet &ns);
51 
52  private:
53  typedef std::vector<std::set<irep_idt>> stack_caughtt;
55  std::set<irep_idt> thrown;
57 };
58 
62 {
63 public:
64  typedef std::map<irep_idt, std::set<irep_idt>> exceptions_mapt;
65 
67  const goto_functionst &,
68  const namespacet &);
69 
70  void output(const goto_functionst &) const;
71 
72  void operator()(
73  const goto_functionst &,
74  const namespacet &,
75  exceptions_mapt &);
76 
78 
79  private:
82 };
83 
85  const goto_functionst &,
86  const namespacet &,
87  std::map<irep_idt, std::set<irep_idt>> &);
88 
89 #endif
uncaught_exceptions_domaint::make_top
void make_top()
Definition: uncaught_exceptions_analysis.h:38
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
uncaught_exceptions_analysist::operator()
void operator()(const goto_functionst &, const namespacet &, exceptions_mapt &)
Applies the uncaught exceptions analysis and outputs the result.
Definition: uncaught_exceptions_analysis.cpp:241
typet
The type of an expression, extends irept.
Definition: type.h:28
uncaught_exceptions_analysist::output
void output(const goto_functionst &) const
Prints the exceptions map that maps each method to the set of exceptions that may escape it.
Definition: uncaught_exceptions_analysis.cpp:213
uncaught_exceptions_domaint::get_elements
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
Definition: uncaught_exceptions_analysis.cpp:165
exprt
Base class for all expressions.
Definition: expr.h:54
uncaught_exceptions_domaint::transform
void transform(const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &)
The transformer for the uncaught exceptions domain.
Definition: uncaught_exceptions_analysis.cpp:63
uncaught_exceptions_analysist::collect_uncaught_exceptions
void collect_uncaught_exceptions(const goto_functionst &, const namespacet &)
Runs the uncaught exceptions analysis, which populates the exceptions map.
Definition: uncaught_exceptions_analysis.cpp:178
uncaught_exceptions_domaint::thrown
std::set< irep_idt > thrown
Definition: uncaught_exceptions_analysis.h:55
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
uncaught_exceptions_domaint::stack_caught
stack_caughtt stack_caught
Definition: uncaught_exceptions_analysis.h:54
uncaught_exceptions_domaint::join
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
Definition: uncaught_exceptions_analysis.cpp:43
uncaught_exceptions_domaint::get_exception_type
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
Definition: uncaught_exceptions_analysis.cpp:23
uncaught_exceptions_domaint::stack_caughtt
std::vector< std::set< irep_idt > > stack_caughtt
Definition: uncaught_exceptions_analysis.h:53
uncaught_exceptions_domaint::class_hierarchy
class_hierarchyt class_hierarchy
Definition: uncaught_exceptions_analysis.h:56
uncaught_exceptions_analysist::exceptions_mapt
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
Definition: uncaught_exceptions_analysis.h:64
uncaught_exceptions_domaint::get_exception_symbol
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
Definition: uncaught_exceptions_analysis.cpp:34
goto_program.h
Concrete Goto Program.
uncaught_exceptions_analysist::domain
uncaught_exceptions_domaint domain
Definition: uncaught_exceptions_analysis.h:80
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
class_hierarchy.h
Class Hierarchy.
uncaught_exceptions
void uncaught_exceptions(const goto_functionst &, const namespacet &, std::map< irep_idt, std::set< irep_idt >> &)
Applies the uncaught exceptions analysis and outputs the result.
Definition: uncaught_exceptions_analysis.cpp:253
uncaught_exceptions_analysist::exceptions_map
exceptions_mapt exceptions_map
Definition: uncaught_exceptions_analysis.h:81
uncaught_exceptions_domaint::operator()
void operator()(const namespacet &ns)
Constructs the class hierarchy.
Definition: uncaught_exceptions_analysis.cpp:171
uncaught_exceptions_domaint
Definition: uncaught_exceptions_analysis.h:28
uncaught_exceptions_analysist
computes in exceptions_map an overapproximation of the exceptions thrown by each method
Definition: uncaught_exceptions_analysis.h:62
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647