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 <algorithm>
16 #include <map>
17 #include <set>
20 
23 
25 {
26  public:
29  const namespacet &);
30 
31  void join(const irep_idt &);
32  void join(const std::set<irep_idt> &);
33  void join(const std::vector<irep_idt> &);
34 
35  void make_top()
36  {
37  thrown.clear();
38  stack_caught.clear();
39  }
40 
41  static irep_idt get_exception_type(const typet &type);
42 
43  static exprt get_exception_symbol(const exprt &exor);
44 
45  const std::set<irep_idt> &get_elements() const;
46 
47  void operator()(const namespacet &ns);
48 
49  private:
50  typedef std::vector<std::set<irep_idt>> stack_caughtt;
52  std::set<irep_idt> thrown;
54 };
55 
59 {
60 public:
61  typedef std::map<irep_idt, std::set<irep_idt>> exceptions_mapt;
62 
64  const goto_functionst &,
65  const namespacet &);
66 
67  void output(const goto_functionst &) const;
68 
69  void operator()(
70  const goto_functionst &,
71  const namespacet &,
72  exceptions_mapt &);
73 
75 
76  private:
79 };
80 
82  const goto_functionst &,
83  const namespacet &,
84  std::map<irep_idt, std::set<irep_idt>> &);
85 
86 #endif
The type of an expression.
Definition: type.h:22
void output(const goto_functionst &) const
Prints the exceptions map that maps each method to the set of exceptions that may escape it...
Goto Programs with Functions.
void transform(const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &)
The transformer for the uncaught exceptions domain.
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
Class Hierarchy.
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
std::vector< std::set< irep_idt > > stack_caughtt
instructionst::const_iterator const_targett
Definition: goto_program.h:398
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void collect_uncaught_exceptions(const goto_functionst &, const namespacet &)
Runs the uncaught exceptions analysis, which populates the exceptions map.
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
void operator()(const namespacet &ns)
Constructs the class hierarchy.
void operator()(const goto_functionst &, const namespacet &, exceptions_mapt &)
Applies the uncaught exceptions analysis and outputs the result.
Base class for all expressions.
Definition: expr.h:42
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.
computes in exceptions_map an overapproximation of the exceptions thrown by each method ...