CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <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
21exprt 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);
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);
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
83
84 if(width_suffix<=config.ansi_c.int_width)
86 else if(width_suffix<=config.ansi_c.long_int_width)
88 else
90
91 bitvector_typet type(
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;
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;
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;
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;
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;
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;
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;
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;
162 }
163 else
165 }
166
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}
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:562
Base class of fixed-width bit-vector types.
Definition std_types.h:909
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
Complex numbers made of pair of given subtype.
Definition std_types.h:1133
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:56
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