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
uncaught_exceptions_domaint::make_top
void make_top()
Definition: uncaught_exceptions_analysis.h:35
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:237
typet
The type of an expression, extends irept.
Definition: type.h:29
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:209
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:161
exprt
Base class for all expressions.
Definition: expr.h:53
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:58
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:174
uncaught_exceptions_domaint::thrown
std::set< irep_idt > thrown
Definition: uncaught_exceptions_analysis.h:52
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
uncaught_exceptions_domaint::stack_caught
stack_caughtt stack_caught
Definition: uncaught_exceptions_analysis.h:51
uncaught_exceptions_domaint::join
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
Definition: uncaught_exceptions_analysis.cpp:38
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:18
uncaught_exceptions_domaint::stack_caughtt
std::vector< std::set< irep_idt > > stack_caughtt
Definition: uncaught_exceptions_analysis.h:50
uncaught_exceptions_domaint::class_hierarchy
class_hierarchyt class_hierarchy
Definition: uncaught_exceptions_analysis.h:53
uncaught_exceptions_analysist::exceptions_mapt
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
Definition: uncaught_exceptions_analysis.h:61
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:29
uncaught_exceptions_analysist::domain
uncaught_exceptions_domaint domain
Definition: uncaught_exceptions_analysis.h:77
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:249
uncaught_exceptions_analysist::exceptions_map
exceptions_mapt exceptions_map
Definition: uncaught_exceptions_analysis.h:78
uncaught_exceptions_domaint::operator()
void operator()(const namespacet &ns)
Constructs the class hierarchy.
Definition: uncaught_exceptions_analysis.cpp:167
uncaught_exceptions_domaint
Definition: uncaught_exceptions_analysis.h:25
goto_functions.h
Goto Programs with Functions.
uncaught_exceptions_analysist
computes in exceptions_map an overapproximation of the exceptions thrown by each method
Definition: uncaught_exceptions_analysis.h:59
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580