1extern int nondet_int(void);
2void __VERIFIER_assert(int cond) {
3 if (!(cond)) {
4 ERROR: goto ERROR;
5 }
6 return;
7}
8
9
10
11unsigned int base2flt(unsigned int m , int e )
12{ unsigned int res ;
13 unsigned int __retres4 ;
14
15 {
16 if (! m) {
17 __retres4 = 0U;
18 goto return_label;
19 } else {
20
21 }
22 if (m < 1U << 24U) {
23 {
24 while (1) {
25 while_0_continue: ;
26 if (e <= -128) {
27 __retres4 = 0U;
28 goto return_label;
29 } else {
30
31 }
32 e = e - 1;
33 m = m << 1U;
34 if (m < 1U << 24U) {
35
36 } else {
37 goto while_0_break;
38 }
39 }
40 while_0_break: ;
41 }
42 } else {
43 {
44 while (1) {
45 while_1_continue: ;
46 if (m >= 1U << 25U) {
47
48 } else {
49 goto while_1_break;
50 }
51 if (e >= 127) {
52 __retres4 = 4294967295U;
53 goto return_label;
54 } else {
55
56 }
57 e = e + 1;
58 m = m >> 1U;
59 }
60 while_1_break: ;
61 }
62 }
63 m = m & ~ (1U << 24U);
64 res = m | (unsigned int )((e + 128) << 24U);
65 __retres4 = res;
66 return_label:
67 return (__retres4);
68}
69}
70unsigned int addflt(unsigned int a , unsigned int b )
71{ unsigned int res ;
72 unsigned int ma ;
73 unsigned int mb ;
74 unsigned int delta ;
75 int ea ;
76 int eb ;
77 unsigned int tmp ;
78 unsigned int __retres10 ;
79
80 {
81 if (a < b) {
82 tmp = a;
83 a = b;
84 b = tmp;
85 } else {
86
87 }
88 if (! b) {
89 __retres10 = a;
90 goto return_label;
91 } else {
92
93 }
94 {
95 ma = a & ((1U << 24U) - 1U);
96 ea = (int )(a >> 24U) - 128;
97 ma = ma | (1U << 24U);
98 mb = b & ((1U << 24U) - 1U);
99 eb = (int )(b >> 24U) - 128;
100 mb = mb | (1U << 24U);
101 __VERIFIER_assert(ea >= eb);
102 delta = ea - eb;
103 mb = mb >> delta;
104 }
105 if (! mb) {
106 __retres10 = a;
107 goto return_label;
108 } else {
109
110 }
111 ma = ma + mb;
112 if (ma & (1U << 25U)) {
113 if (ea == 127) {
114 __retres10 = 4294967295U;
115 goto return_label;
116 } else {
117
118 }
119 ea = ea + 1;
120 ma = ma >> 1U;
121 } else {
122
123 }
124 {
125 __VERIFIER_assert(ma < 1U << 25U);
126 ma = ma & ((1U << 24U) - 1U);
127 res = ma | (unsigned int )((ea + 128) << 24U);
128 }
129 __retres10 = res;
130 return_label:
131 return (__retres10);
132}
133}
134unsigned int mulflt(unsigned int a , unsigned int b )
135{ unsigned int res ;
136 unsigned int ma ;
137 unsigned int mb ;
138 unsigned long long accu ;
139 int ea ;
140 int eb ;
141 unsigned int tmp ;
142 unsigned int __retres10 ;
143
144 {
145 if (a < b) {
146 tmp = a;
147 a = b;
148 b = tmp;
149 } else {
150
151 }
152 if (! b) {
153 __retres10 = 0U;
154 goto return_label;
155 } else {
156
157 }
158 ma = a & ((1U << 24U) - 1U);
159 ea = (int )(a >> 24U) - 128;
160 ma = ma | (1U << 24U);
161 mb = b & ((1U << 24U) - 1U);
162 eb = (int )(b >> 24U) - 128;
163 mb = mb | (1U << 24U);
164 ea = ea + eb;
165 ea = ea + 24;
166 if (ea > 127) {
167 __retres10 = 4294967295U;
168 goto return_label;
169 } else {
170
171 }
172 if (ea < -128) {
173 __retres10 = 0U;
174 goto return_label;
175 } else {
176
177 }
178 accu = ma;
179 accu = accu * (unsigned long long )mb;
180 accu = accu >> 24U;
181 if (accu >= (unsigned long long )(1U << 25U)) {
182 if (ea == 127) {
183 __retres10 = 4294967295U;
184 goto return_label;
185 } else {
186
187 }
188 ea = ea + 1;
189 accu = accu >> 1U;
190 if (accu >= (unsigned long long )(1U << 25U)) {
191 __retres10 = 4294967295U;
192 goto return_label;
193 } else {
194
195 }
196 } else {
197
198 }
199 {
200 __VERIFIER_assert(accu < (unsigned long long )(1U << 25U));
201 __VERIFIER_assert(accu & (unsigned long long )(1U << 24U));
202 ma = accu;
203 ma = ma & ~ (1U << 24U);
204 res = ma | (unsigned int )((ea + 128) << 24U);
205 }
206 __retres10 = res;
207 return_label:
208 return (__retres10);
209}
210}
211int main(void)
212{ unsigned int a ;
213 unsigned int ma ;
214 signed char ea ;
215 unsigned int b ;
216 unsigned int mb ;
217 signed char eb ;
218 unsigned int r_add ;
219 unsigned int zero ;
220 int sa ;
221 int sb ;
222 int tmp ;
223 int tmp___0 ;
224 int tmp___1 ;
225 int tmp___2 ;
226 int tmp___3 ;
227 int tmp___4 ;
228 int tmp___5 ;
229 int tmp___6 ;
230 int tmp___7 ;
231 int tmp___8 ;
232 int tmp___9 ;
233 int __retres23 ;
234
235 {
236 {
237 zero = base2flt(0, 0);
238 a = base2flt(ma, ea);
239 b = base2flt(mb, eb);
240 }
241 if (a < zero) {
242 sa = -1;
243 } else {
244 if (a > zero) {
245 tmp = 1;
246 } else {
247 tmp = 0;
248 }
249 sa = tmp;
250 }
251 if (b < zero) {
252 sb = -1;
253 } else {
254 if (b > zero) {
255 tmp___0 = 1;
256 } else {
257 tmp___0 = 0;
258 }
259 sb = tmp___0;
260 }
261 {
262 r_add = addflt(a, b);
263 }
264 if (sa > 0) {
265 if (sb > 0) {
266 if (r_add < a) {
267 tmp___2 = -1;
268 } else {
269 if (r_add > a) {
270 tmp___1 = 1;
271 } else {
272 tmp___1 = 0;
273 }
274 tmp___2 = tmp___1;
275 }
276 {
277 __VERIFIER_assert(tmp___2 >= 0);
278 }
279 if (r_add < b) {
280 tmp___4 = -1;
281 } else {
282 if (r_add > b) {
283 tmp___3 = 1;
284 } else {
285 tmp___3 = 0;
286 }
287 tmp___4 = tmp___3;
288 }
289 {
290 __VERIFIER_assert(tmp___4 >= 0);
291 }
292 } else {
293
294 }
295 } else {
296
297 }
298 if (sa == 0) {
299 goto _L;
300 } else {
301 if (sb == 0) {
302 _L:
303 if (r_add < a) {
304 tmp___6 = -1;
305 } else {
306 if (r_add > a) {
307 tmp___5 = 1;
308 } else {
309 tmp___5 = 0;
310 }
311 tmp___6 = tmp___5;
312 }
313 if (tmp___6 == 0) {
314 tmp___9 = 1;
315 } else {
316 if (r_add < b) {
317 tmp___8 = -1;
318 } else {
319 if (r_add > b) {
320 tmp___7 = 1;
321 } else {
322 tmp___7 = 0;
323 }
324 tmp___8 = tmp___7;
325 }
326 if (tmp___8 == 0) {
327 tmp___9 = 1;
328 } else {
329 tmp___9 = 0;
330 }
331 }
332 {
333 __VERIFIER_assert(tmp___9);
334 }
335 } else {
336
337 }
338 }
339 __retres23 = 0;
340 return (__retres23);
341}
342}