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