CBMC
Loading...
Searching...
No Matches
convert_integer_literal.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Conversion
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
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
22exprt 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);
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);
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
84
85 if(width_suffix<=config.ansi_c.int_width)
87 else if(width_suffix<=config.ansi_c.long_int_width)
89 else
91
92 bitvector_typet type(
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;
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;
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;
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;
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;
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;
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;
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;
163 }
164 else
166 }
167
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}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Base class of fixed-width bit-vector types.
Complex constructor from a pair of numbers.
Definition std_expr.h:1849
Complex numbers made of pair of given subtype.
Definition std_types.h:1074
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
#define FITS(width, signed)
exprt convert_integer_literal(const std::string &src)
C++ Language Conversion.
int isdigit(int c)
Definition ctype.c:24
int tolower(int c)
Definition ctype.c:109
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
BigInt mp_integer
Definition smt_terms.h:17
API to expression classes.
unsigned unsafe_string2unsigned(const std::string &str, int base)
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45
bool is_unsigned(const typet &t)
Convenience function – is the type unsigned?
Definition util.cpp:52