cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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/namespace.h
>
17
#include <
util/std_types.h
>
18
20
void
cpp_exception_list_rec
(
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
{
28
if
(src.
get_bool
(ID_C_reference))
29
{
30
// do not change
31
cpp_exception_list_rec
(
32
to_reference_type
(src).base_type(), ns, suffix, dest);
33
}
34
else
35
{
36
// append suffix _ptr
37
cpp_exception_list_rec
(
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
66
irep_idt
c_type=src.
get
(ID_C_c_type);
67
68
if
(!c_type.
empty
())
69
{
70
dest.push_back(
id2string
(c_type)+suffix);
71
return
;
72
}
73
}
74
}
75
77
irept
cpp_exception_list
(
78
const
typet
&src,
79
const
namespacet
&ns)
80
{
81
std::vector<irep_idt> ids;
82
irept
result(ID_exception_list);
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
94
irep_idt
cpp_exception_id
(
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
}
c_types.h
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:224
dstringt::empty
bool empty() const
Definition
dstring.h:89
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition
irep.cpp:57
irept::get
const irep_idt & get(const irep_idt &name) const
Definition
irep.cpp:44
irept::get_sub
subt & get_sub()
Definition
irep.h:448
irept::id
const irep_idt & id() const
Definition
irep.h:388
irept::get_string
const std::string & get_string(const irep_idt &name) const
Definition
irep.h:401
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition
namespace.cpp:49
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
typet
The type of an expression, extends irept.
Definition
type.h:29
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:94
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:20
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:77
cpp_exception_id.h
C++ Language Type Checking.
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
namespace.h
to_reference_type
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition
pointer_expr.h:162
invariant.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition
invariant.h:495
std_types.h
Pre-defined types.
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition
std_types.h:308
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:518
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
cpp
cpp_exception_id.cpp
Generated by
1.17.0