cprover
Loading...
Searching...
No Matches
parse_float.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Conversion of Expressions
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "parse_float.h"
13
14#include <algorithm>
15#include <cctype>
16#include <cstring>
17
18parse_floatt::parse_floatt(const std::string &src)
19{
20 // {digits}{dot}{digits}{exponent}?{floatsuffix}?
21 // {digits}{dot}{exponent}?{floatsuffix}?
22 // {dot}{digits}{exponent}?{floatsuffix}?
23 // {digits}{exponent}{floatsuffix}?
24
25 // Hex format (C99):
26 // 0x{hexdigits}{dot}{hexdigits}[pP]{exponent}{floatsuffix}?
27 // 0x{hexdigits}{dot}[pP]{exponent}{floatsuffix}?
28
29 // These are case-insensitive, and we handle this
30 // by first converting to lower case.
31
32 std::string src_lower=src;
33 std::transform(src_lower.begin(), src_lower.end(),
34 src_lower.begin(), ::tolower);
35
36 const char *p=src_lower.c_str();
37
38 std::string str_whole_number,
41
43
44 // is this hex?
45
46 if(src_lower.size()>=2 && src_lower[0]=='0' && src_lower[1]=='x')
47 {
48 // skip the 0x
49 p+=2;
50
52
53 // get whole number part
54 while(*p!='.' && *p!=0 && *p!='p')
55 {
57 p++;
58 }
59
60 // skip dot
61 if(*p=='.')
62 p++;
63
64 // get fraction part
65 while(*p!=0 && *p!='p')
66 {
68 p++;
69 }
70
71 // skip p
72 if(*p=='p')
73 p++;
74
75 // skip +
76 if(*p=='+')
77 p++;
78
79 // get exponent
80 while(*p!=0 && *p!='f' && *p!='l' &&
81 *p!='w' && *p!='q' && *p!='d')
82 {
83 str_exponent+=*p;
84 p++;
85 }
86
87 std::string str_number=str_whole_number+
89
90 // The significand part is interpreted as a (decimal or hexadecimal)
91 // rational number; the digit sequence in the exponent part is
92 // interpreted as a decimal integer.
93
94 if(str_number.empty())
96 else
98
99 if(str_exponent.empty())
100 exponent=0;
101 else
102 exponent=string2integer(str_exponent, 10); // decimal
103
104 // adjust exponent
105 exponent-=str_fraction_part.size()*4; // each digit has 4 bits
106 }
107 else
108 {
109 // get whole number part
110 while(*p!='.' && *p!=0 && *p!='e' &&
111 *p!='f' && *p!='l' &&
112 *p!='w' && *p!='q' && *p!='d' &&
113 *p!='i' && *p!='j')
114 {
116 p++;
117 }
118
119 // skip dot
120 if(*p=='.')
121 p++;
122
123 // get fraction part
124 while(*p!=0 && *p!='e' &&
125 *p!='f' && *p!='l' &&
126 *p!='w' && *p!='q' && *p!='d' &&
127 *p!='i' && *p!='j')
128 {
130 p++;
131 }
132
133 // skip e
134 if(*p=='e')
135 p++;
136
137 // skip +
138 if(*p=='+')
139 p++;
140
141 // get exponent
142 while(*p!=0 && *p!='f' && *p!='l' &&
143 *p!='w' && *p!='q' && *p!='d' &&
144 *p!='i' && *p!='j')
145 {
146 str_exponent+=*p;
147 p++;
148 }
149
150 std::string str_number=str_whole_number+
152
153 if(str_number.empty())
154 significand=0;
155 else
157
158 if(str_exponent.empty())
159 exponent=0;
160 else
162
163 // adjust exponent
165 }
166
167 // get flags
168 is_float=is_long=false;
170 is_float16=false;
173 is_float80=false;
175
176 if(strcmp(p, "f16")==0)
177 is_float16=true;
178 else if(strcmp(p, "f32")==0)
179 is_float32=true;
180 else if(strcmp(p, "f32x")==0)
181 is_float32x=true;
182 else if(strcmp(p, "f64")==0)
183 is_float64=true;
184 else if(strcmp(p, "f64x")==0)
185 is_float64x=true;
186 else if(strcmp(p, "f128")==0)
187 is_float128=true;
188 else if(strcmp(p, "f128x")==0)
189 is_float128x=true;
190 else
191 {
192 while(*p!=0)
193 {
194 if(*p=='f')
195 is_float=true;
196 else if(*p=='l')
197 is_long=true;
198 else if(*p=='i' || *p=='j')
199 is_imaginary=true;
200 // http://gcc.gnu.org/onlinedocs/gcc/Decimal-Float.html
201 else if(*p=='d')
202 // a suffix with just d or D but nothing else is a GCC extension with no
203 // particular effect -- and forbidden by Clang
204 is_decimal=is_decimal || *(p+1)!=0;
205 // http://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
206 else if(*p=='w')
207 is_float80=true;
208 else if(*p=='q')
209 is_float128=true;
210
211 p++;
212 }
213 }
214}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
bool is_imaginary
Definition parse_float.h:28
unsigned exponent_base
Definition parse_float.h:23
mp_integer significand
Definition parse_float.h:22
parse_floatt(const std::string &)
mp_integer exponent
Definition parse_float.h:22
bool is_float128x
Definition parse_float.h:32
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
ANSI-C Conversion / Type Checking.