CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_exception_id.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: 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/namespace.h>
17#include <util/std_types.h>
18
21 const typet &src,
22 const namespacet &ns,
23 const std::string &suffix,
24 std::vector<irep_idt> &dest)
25{
26 if(src.id() == ID_pointer)
27 {
29 {
30 // do not change
32 to_reference_type(src).base_type(), ns, suffix, dest);
33 }
34 else
35 {
36 // append suffix _ptr
38 to_reference_type(src).base_type(), ns, "_ptr" + suffix, dest);
39 }
40 }
41 else if(src.id() == ID_union_tag)
42 {
43 cpp_exception_list_rec(ns.follow_tag(to_union_tag_type(src)), ns, suffix, dest);
44 }
45 else if(src.id()==ID_union)
46 {
47 // just get tag
48 dest.push_back("union_"+src.get_string(ID_tag));
49 }
50 else if(src.id() == ID_struct_tag)
51 {
52 cpp_exception_list_rec(ns.follow_tag(to_struct_tag_type(src)), ns, suffix, dest);
53 }
54 else if(src.id()==ID_struct)
55 {
56 // just get tag
57 dest.push_back("struct_"+src.get_string(ID_tag));
58
59 // now do any bases, recursively
60 for(const auto &b : to_struct_type(src).bases())
61 cpp_exception_list_rec(b.type(), ns, suffix, dest);
62 }
63 else
64 {
65 // grab C/C++ type
67
68 if(!c_type.empty())
69 {
70 dest.push_back(id2string(c_type)+suffix);
71 return;
72 }
73 }
74}
75
78 const typet &src,
79 const namespacet &ns)
80{
81 std::vector<irep_idt> ids;
83
84 cpp_exception_list_rec(src, ns, "", ids);
85 result.get_sub().resize(ids.size());
86
87 for(std::size_t i=0; i<ids.size(); i++)
88 result.get_sub()[i].id(ids[i]);
89
90 return result;
91}
92
95 const typet &src,
96 const namespacet &ns)
97{
98 std::vector<irep_idt> ids;
99 cpp_exception_list_rec(src, ns, "", ids);
100 CHECK_RETURN(!ids.empty());
101 return ids.front();
102}
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
subt & get_sub()
Definition irep.h:448
const irep_idt & id() const
Definition irep.h:388
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29
irep_idt cpp_exception_id(const typet &src, const namespacet &ns)
turns a type into an exception ID
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
irept cpp_exception_list(const typet &src, const namespacet &ns)
turns a type into a list of relevant exception IDs
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518