cprover
cpp_exception_id.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_exception_id.h"
13 
14 #include <util/c_types.h>
15 #include <util/invariant.h>
16 #include <util/std_types.h>
17 
20  const typet &src,
21  const namespacet &ns,
22  const std::string &suffix,
23  std::vector<irep_idt> &dest)
24 {
25  if(src.id() == ID_pointer)
26  {
27  if(src.get_bool(ID_C_reference))
28  {
29  // do not change
30  cpp_exception_list_rec(src.subtype(), ns, suffix, dest);
31  }
32  else
33  {
34  // append suffix _ptr
35  cpp_exception_list_rec(src.subtype(), ns, "_ptr"+suffix, dest);
36  }
37  }
38  else if(src.id() == ID_union_tag)
39  {
40  cpp_exception_list_rec(ns.follow_tag(to_union_tag_type(src)), ns, suffix, dest);
41  }
42  else if(src.id()==ID_union)
43  {
44  // just get tag
45  dest.push_back("union_"+src.get_string(ID_tag));
46  }
47  else if(src.id() == ID_struct_tag)
48  {
49  cpp_exception_list_rec(ns.follow_tag(to_struct_tag_type(src)), ns, suffix, dest);
50  }
51  else if(src.id()==ID_struct)
52  {
53  // just get tag
54  dest.push_back("struct_"+src.get_string(ID_tag));
55 
56  // now do any bases, recursively
57  for(const auto &b : to_struct_type(src).bases())
58  cpp_exception_list_rec(b.type(), ns, suffix, dest);
59  }
60  else
61  {
62  // grab C/C++ type
63  irep_idt c_type=src.get(ID_C_c_type);
64 
65  if(!c_type.empty())
66  {
67  dest.push_back(id2string(c_type)+suffix);
68  return;
69  }
70  }
71 }
72 
75  const typet &src,
76  const namespacet &ns)
77 {
78  std::vector<irep_idt> ids;
79  irept result(ID_exception_list);
80 
81  cpp_exception_list_rec(src, ns, "", ids);
82  result.get_sub().resize(ids.size());
83 
84  for(std::size_t i=0; i<ids.size(); i++)
85  result.get_sub()[i].id(ids[i]);
86 
87  return result;
88 }
89 
92  const typet &src,
93  const namespacet &ns)
94 {
95  std::vector<irep_idt> ids;
96  cpp_exception_list_rec(src, ns, "", ids);
97  CHECK_RETURN(!ids.empty());
98  return ids.front();
99 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
cpp_exception_id
irep_idt cpp_exception_id(const typet &src, const namespacet &ns)
turns a type into an exception ID
Definition: cpp_exception_id.cpp:91
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
invariant.h
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
cpp_exception_id.h
C++ Language Type Checking.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
cpp_exception_list
irept cpp_exception_list(const typet &src, const namespacet &ns)
turns a type into a list of relevant exception IDs
Definition: cpp_exception_id.cpp:74
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
std_types.h
Pre-defined types.
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
dstringt::empty
bool empty() const
Definition: dstring.h:88
cpp_exception_list_rec
void cpp_exception_list_rec(const typet &src, const namespacet &ns, const std::string &suffix, std::vector< irep_idt > &dest)
turns a type into a list of relevant exception IDs
Definition: cpp_exception_id.cpp:19
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
irept::get_sub
subt & get_sub()
Definition: irep.h:467
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
c_types.h