cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
convert_integer_literal.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: C++ Language Conversion
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
convert_integer_literal.h
"
13
14
#include <
util/arith_tools.h
>
15
#include <
util/c_types.h
>
// IWYU pragma: keep
16
#include <
util/config.h
>
17
#include <
util/std_expr.h
>
18
#include <
util/string2int.h
>
19
20
#include <cctype>
21
22
exprt
convert_integer_literal
(
const
std::string &src)
23
{
24
bool
is_unsigned
=
false
, is_imaginary=
false
;
25
unsigned
long_cnt=0;
26
unsigned
width_suffix=0;
27
unsigned
base=10;
28
29
for
(
unsigned
i=0; i<src.size(); i++)
30
{
31
char
ch=src[i];
32
33
if
(ch==
'u'
|| ch==
'U'
)
34
is_unsigned
=
true
;
35
else
if
(ch==
'l'
|| ch==
'L'
)
36
long_cnt++;
37
else
if
(ch==
'i'
|| ch==
'I'
)
38
{
39
// This can be "1i128" in MS mode,
40
// and "10i" (imaginary) for GCC.
41
// If it's followed by a number, we do MS mode.
42
if
((i+1)<src.size() && isdigit(src[i+1]))
43
width_suffix=
unsafe_string2unsigned
(src.substr(i+1));
44
else
45
is_imaginary=
true
;
46
}
47
else
if
(ch==
'j'
|| ch==
'J'
)
48
is_imaginary=
true
;
49
}
50
51
mp_integer
value;
52
53
if
(src.size()>=2 && src[0]==
'0'
&& tolower(src[1])==
'x'
)
54
{
55
// hex; strip "0x"
56
base=16;
57
std::string without_prefix(src, 2, std::string::npos);
58
value=
string2integer
(without_prefix, 16);
59
}
60
else
if
(src.size()>=2 && src[0]==
'0'
&& tolower(src[1])==
'b'
)
61
{
62
// binary; strip "0x"
63
// see http://gcc.gnu.org/onlinedocs/gcc/Binary-constants.html
64
base=2;
65
std::string without_prefix(src, 2, std::string::npos);
66
value=
string2integer
(without_prefix, 2);
67
}
68
else
if
(src.size()>=2 && src[0]==
'0'
&& isdigit(src[1]))
69
{
70
// octal
71
base=8;
72
value=
string2integer
(src, 8);
73
}
74
else
75
{
76
// The default is base 10.
77
value=
string2integer
(src, 10);
78
}
79
80
if
(width_suffix!=0)
81
{
82
// this is a Microsoft extension
83
irep_idt
c_type;
84
85
if
(width_suffix<=
config
.ansi_c.int_width)
86
c_type=
is_unsigned
?ID_unsigned_int:ID_signed_int;
87
else
if
(width_suffix<=
config
.ansi_c.long_int_width)
88
c_type=
is_unsigned
?ID_unsigned_long_int:ID_signed_long_int;
89
else
90
c_type=
is_unsigned
?ID_unsigned_long_long_int:ID_signed_long_long_int;
91
92
bitvector_typet
type(
93
is_unsigned
? ID_unsignedbv : ID_signedbv, width_suffix);
94
type.
set
(ID_C_c_type, c_type);
95
96
exprt
result=
from_integer
(value, type);
97
98
return
result;
99
}
100
101
mp_integer
value_abs=value;
102
103
if
(value<0)
104
value_abs.negate();
105
106
bool
is_hex_or_oct_or_bin=(base==8) || (base==16) || (base==2);
107
108
#define FITS(width, signed) \
109
((signed?!is_unsigned:(is_unsigned || is_hex_or_oct_or_bin)) && \
110
(power(2, signed?width-1:width)>value_abs))
111
112
unsigned
width;
113
bool
is_signed
=
false
;
114
irep_idt
c_type;
115
116
if
(
FITS
(
config
.ansi_c.int_width,
true
) && long_cnt==0)
// int
117
{
118
width=
config
.ansi_c.int_width;
119
is_signed
=
true
;
120
c_type=ID_signed_int;
121
}
122
else
if
(
FITS
(
config
.ansi_c.int_width,
false
) && long_cnt==0)
// unsigned int
123
{
124
width=
config
.ansi_c.int_width;
125
is_signed
=
false
;
126
c_type=ID_unsigned_int;
127
}
128
else
if
(
FITS
(
config
.ansi_c.long_int_width,
true
) && long_cnt!=2)
// long int
129
{
130
width=
config
.ansi_c.long_int_width;
131
is_signed
=
true
;
132
c_type=ID_signed_long_int;
133
}
134
// unsigned long int
135
else
if
(
FITS
(
config
.ansi_c.long_int_width,
false
) && long_cnt!=2)
136
{
137
width=
config
.ansi_c.long_int_width;
138
is_signed
=
false
;
139
c_type=ID_unsigned_long_int;
140
}
141
else
if
(
FITS
(
config
.ansi_c.long_long_int_width,
true
))
// long long int
142
{
143
width=
config
.ansi_c.long_long_int_width;
144
is_signed
=
true
;
145
c_type=ID_signed_long_long_int;
146
}
147
// unsigned long long int
148
else
if
(
FITS
(
config
.ansi_c.long_long_int_width,
false
))
149
{
150
width=
config
.ansi_c.long_long_int_width;
151
is_signed
=
false
;
152
c_type=ID_unsigned_long_long_int;
153
}
154
else
155
{
156
// Way too large. Should consider issuing a warning.
157
width=
config
.ansi_c.long_long_int_width;
158
159
if
(
is_unsigned
)
160
{
161
is_signed
=
false
;
162
c_type=ID_unsigned_long_long_int;
163
}
164
else
165
c_type=ID_signed_long_long_int;
166
}
167
168
bitvector_typet
type(
is_signed
? ID_signedbv : ID_unsignedbv, width);
169
type.
set
(ID_C_c_type, c_type);
170
171
exprt
result;
172
173
if
(is_imaginary)
174
{
175
result =
complex_exprt
(
176
from_integer
(0, type),
from_integer
(value, type),
complex_typet
(type));
177
}
178
else
179
{
180
result=
from_integer
(value, type);
181
result.
set
(ID_C_base, base);
182
}
183
184
return
result;
185
}
config
configt config
Definition
config.cpp:25
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition
arith_tools.cpp:100
arith_tools.h
c_types.h
bitvector_typet
Base class of fixed-width bit-vector types.
Definition
bitvector_types.h:27
complex_exprt
Complex constructor from a pair of numbers.
Definition
std_expr.h:1859
complex_typet
Complex numbers made of pair of given subtype.
Definition
std_types.h:1023
exprt
Base class for all expressions.
Definition
expr.h:57
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition
irep.h:412
config.h
FITS
#define FITS(width, signed)
convert_integer_literal
exprt convert_integer_literal(const std::string &src)
Definition
convert_integer_literal.cpp:22
convert_integer_literal.h
C++ Language Conversion.
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition
mp_arith.cpp:54
mp_integer
BigInt mp_integer
Definition
smt_terms.h:17
std_expr.h
API to expression classes.
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition
string2int.cpp:35
string2int.h
is_signed
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition
util.cpp:45
is_unsigned
bool is_unsigned(const typet &t)
Convenience function – is the type unsigned?
Definition
util.cpp:52
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
ansi-c
literals
convert_integer_literal.cpp
Generated by
1.17.0