-
Notifications
You must be signed in to change notification settings - Fork 300
Expand file tree
/
Copy pathformat_type.cpp
More file actions
128 lines (113 loc) · 3.58 KB
/
Copy pathformat_type.cpp
File metadata and controls
128 lines (113 loc) · 3.58 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
/*******************************************************************\
Module:
Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
#include "format_type.h"
#include "c_types.h"
#include "format_expr.h"
#include "mathematical_types.h"
#include "pointer_expr.h"
#include "std_types.h"
#include <ostream>
/// format a \ref struct_typet
static std::ostream &format_rec(std::ostream &os, const struct_typet &src)
{
os << "struct"
<< " {";
bool first = true;
for(const auto &c : src.components())
{
if(first)
first = false;
else
os << ',';
os << ' ' << format(c.type()) << ' ' << c.get_name();
}
return os << " }";
}
/// format a \ref union_typet
static std::ostream &format_rec(std::ostream &os, const union_typet &src)
{
os << "union"
<< " {";
bool first = true;
for(const auto &c : src.components())
{
if(first)
first = false;
else
os << ',';
os << ' ' << format(c.type()) << ' ' << c.get_name();
}
return os << " }";
}
// The below generates a string in a generic syntax
// that is inspired by C/C++/Java, and is meant for debugging
// purposes.
std::ostream &format_rec(std::ostream &os, const typet &type)
{
const auto &id = type.id();
if(id == ID_pointer)
return os << format(to_pointer_type(type).base_type()) << '*';
else if(id == ID_array)
{
const auto &t = to_array_type(type);
if(t.is_complete())
return os << format(t.element_type()) << '[' << format(t.size()) << ']';
else
return os << format(t.element_type()) << "[]";
}
else if(id == ID_struct)
return format_rec(os, to_struct_type(type));
else if(id == ID_union)
return format_rec(os, to_union_type(type));
else if(id == ID_union_tag)
return os << "union " << to_union_tag_type(type).get_identifier();
else if(id == ID_struct_tag)
return os << "struct " << to_struct_tag_type(type).get_identifier();
else if(id == ID_c_enum_tag)
return os << "c_enum " << to_c_enum_tag_type(type).get_identifier();
else if(id == ID_signedbv)
return os << "signedbv[" << to_signedbv_type(type).get_width() << ']';
else if(id == ID_unsignedbv)
return os << "unsignedbv[" << to_unsignedbv_type(type).get_width() << ']';
else if(id == ID_bv)
return os << "bv[" << to_bitvector_type(type).get_width() << ']';
else if(id == ID_floatbv)
return os << "floatbv[" << to_floatbv_type(type).get_width() << ']';
else if(id == ID_c_bool)
return os << "c_bool[" << to_c_bool_type(type).get_width() << ']';
else if(id == ID_bool)
return os << "\xf0\x9d\x94\xb9"; // u+1D539, 'B'
else if(id == ID_integer)
return os << "\xe2\x84\xa4"; // u+2124, 'Z'
else if(id == ID_natural)
return os << "\xe2\x84\x95"; // u+2115, 'N'
else if(id == ID_range)
{
auto &range_type = to_integer_range_type(type);
return os << "{ " << range_type.from() << ", ..., " << range_type.to()
<< " }";
}
else if(id == ID_rational)
return os << "\xe2\x84\x9a"; // u+211A, 'Q'
else if(id == ID_real)
return os << "\xe2\x84\x9d"; // u+211D, 'R'
else if(id == ID_mathematical_function)
{
const auto &mathematical_function = to_mathematical_function_type(type);
bool first = true;
for(const auto &domain : mathematical_function.domain())
{
if(first)
first = false;
else
os << u8" \u00d7 "; // ×
os << format(domain);
}
os << u8" \u2192 "; // → -- we don't use ⟶ since that doesn't render well
return os << format(mathematical_function.codomain());
}
else
return os << id;
}