Clang Project

clang_source_code/test/Analysis/svalbuilder-rearrange-comparisons.c
1// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-binary-operation-simplification=true -verify -analyzer-config eagerly-assume=false %s
2
3void clang_analyzer_eval(int x);
4void clang_analyzer_denote(int x, const char *literal);
5void clang_analyzer_express(int x);
6
7void exit(int);
8
9#define UINT_MAX (~0U)
10#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
11
12extern void __assert_fail (__const char *__assertion, __const char *__file,
13    unsigned int __line, __const char *__function)
14     __attribute__ ((__noreturn__));
15#define assert(expr) \
16  ((expr)  ? (void)(0)  : __assert_fail (#expr, __FILE__, __LINE__, __func__))
17
18int g();
19int f() {
20  int x = g();
21  // Assert that no overflows occur in this test file.
22  // Assuming that concrete integers are also within that range.
23  assert(x <= ((int)INT_MAX / 4));
24  assert(x >= -((int)INT_MAX / 4));
25  return x;
26}
27
28void compare_different_symbol_equal() {
29  int x = f(), y = f();
30  clang_analyzer_denote(x, "$x");
31  clang_analyzer_denote(y, "$y");
32  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 0}}
33}
34
35void compare_different_symbol_plus_left_int_equal() {
36  int x = f(), y = f();
37  clang_analyzer_denote(x, "$x");
38  clang_analyzer_denote(y, "$y");
39  x += 1;
40  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 1}}
41}
42
43void compare_different_symbol_minus_left_int_equal() {
44  int x = f(), y = f();
45  clang_analyzer_denote(x, "$x");
46  clang_analyzer_denote(y, "$y");
47  x -= 1;
48  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 1}}
49}
50
51void compare_different_symbol_plus_right_int_equal() {
52  int x = f(), y = f();
53  clang_analyzer_denote(x, "$x");
54  clang_analyzer_denote(y, "$y");
55  y += 2;
56  clang_analyzer_express(y); // expected-warning {{$y + 2}}
57  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 2}}
58}
59
60void compare_different_symbol_minus_right_int_equal() {
61  int x = f(), y = f();
62  clang_analyzer_denote(x, "$x");
63  clang_analyzer_denote(y, "$y");
64  y -= 2;
65  clang_analyzer_express(y); // expected-warning {{$y - 2}}
66  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 2}}
67}
68
69void compare_different_symbol_plus_left_plus_right_int_equal() {
70  int x = f(), y = f();
71  clang_analyzer_denote(x, "$x");
72  clang_analyzer_denote(y, "$y");
73  x += 2;
74  y += 1;
75  clang_analyzer_express(x); // expected-warning {{$x + 2}}
76  clang_analyzer_express(y); // expected-warning {{$y + 1}}
77  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 1}}
78}
79
80void compare_different_symbol_plus_left_minus_right_int_equal() {
81  int x = f(), y = f();
82  clang_analyzer_denote(x, "$x");
83  clang_analyzer_denote(y, "$y");
84  x += 2;
85  y -= 1;
86  clang_analyzer_express(x); // expected-warning {{$x + 2}}
87  clang_analyzer_express(y); // expected-warning {{$y - 1}}
88  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 3}}
89}
90
91void compare_different_symbol_minus_left_plus_right_int_equal() {
92  int x = f(), y = f();
93  clang_analyzer_denote(x, "$x");
94  clang_analyzer_denote(y, "$y");
95  x -= 2;
96  y += 1;
97  clang_analyzer_express(x); // expected-warning {{$x - 2}}
98  clang_analyzer_express(y); // expected-warning {{$y + 1}}
99  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 3}}
100}
101
102void compare_different_symbol_minus_left_minus_right_int_equal() {
103  int x = f(), y = f();
104  clang_analyzer_denote(x, "$x");
105  clang_analyzer_denote(y, "$y");
106  x -= 2;
107  y -= 1;
108  clang_analyzer_express(x); // expected-warning {{$x - 2}}
109  clang_analyzer_express(y); // expected-warning {{$y - 1}}
110  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 1}}
111}
112
113void compare_same_symbol_equal() {
114  int x = f(), y = x;
115  clang_analyzer_denote(x, "$x");
116  clang_analyzer_express(y); // expected-warning {{$x}}
117  clang_analyzer_eval(x == y); // expected-warning {{TRUE}}
118}
119
120void compare_same_symbol_plus_left_int_equal() {
121  int x = f(), y = x;
122  clang_analyzer_denote(x, "$x");
123  ++x;
124  clang_analyzer_express(x); // expected-warning {{$x + 1}}
125  clang_analyzer_express(y); // expected-warning {{$x}}
126  clang_analyzer_eval(x == y); // expected-warning {{FALSE}}
127}
128
129void compare_same_symbol_minus_left_int_equal() {
130  int x = f(), y = x;
131  clang_analyzer_denote(x, "$x");
132  --x;
133  clang_analyzer_express(x); // expected-warning {{$x - 1}}
134  clang_analyzer_express(y); // expected-warning {{$x}}
135  clang_analyzer_eval(x == y); // expected-warning {{FALSE}}
136}
137
138void compare_same_symbol_plus_right_int_equal() {
139  int x = f(), y = x + 1;
140  clang_analyzer_denote(x, "$x");
141  clang_analyzer_express(y); // expected-warning {{$x + 1}}
142  clang_analyzer_eval(x == y); // expected-warning {{FALSE}}
143}
144
145void compare_same_symbol_minus_right_int_equal() {
146  int x = f(), y = x - 1;
147  clang_analyzer_denote(x, "$x");
148  clang_analyzer_express(y); // expected-warning {{$x - 1}}
149  clang_analyzer_eval(x == y); // expected-warning {{FALSE}}
150}
151
152void compare_same_symbol_plus_left_plus_right_int_equal() {
153  int x = f(), y = x + 1;
154  clang_analyzer_denote(x, "$x");
155  ++x;
156  clang_analyzer_express(x); // expected-warning {{$x + 1}}
157  clang_analyzer_express(y); // expected-warning {{$x + 1}}
158  clang_analyzer_eval(x == y); // expected-warning {{TRUE}}
159}
160
161void compare_same_symbol_plus_left_minus_right_int_equal() {
162  int x = f(), y = x - 1;
163  clang_analyzer_denote(x, "$x");
164  ++x;
165  clang_analyzer_express(x); // expected-warning {{$x + 1}}
166  clang_analyzer_express(y); // expected-warning {{$x - 1}}
167  clang_analyzer_eval(x == y); // expected-warning {{FALSE}}
168}
169
170void compare_same_symbol_minus_left_plus_right_int_equal() {
171  int x = f(), y = x + 1;
172  clang_analyzer_denote(x, "$x");
173  --x;
174  clang_analyzer_express(x); // expected-warning {{$x - 1}}
175  clang_analyzer_express(y); // expected-warning {{$x + 1}}
176  clang_analyzer_eval(x == y); // expected-warning {{FALSE}}
177}
178
179void compare_same_symbol_minus_left_minus_right_int_equal() {
180  int x = f(), y = x - 1;
181  clang_analyzer_denote(x, "$x");
182  --x;
183  clang_analyzer_express(x); // expected-warning {{$x - 1}}
184  clang_analyzer_express(y); // expected-warning {{$x - 1}}
185  clang_analyzer_eval(x == y); // expected-warning {{TRUE}}
186}
187
188void compare_different_symbol_less_or_equal() {
189  int x = f(), y = f();
190  clang_analyzer_denote(x, "$x");
191  clang_analyzer_denote(y, "$y");
192  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 0}}
193}
194
195void compare_different_symbol_plus_left_int_less_or_equal() {
196  int x = f(), y = f();
197  clang_analyzer_denote(x, "$x");
198  clang_analyzer_denote(y, "$y");
199  x += 1;
200  clang_analyzer_express(x); // expected-warning {{$x + 1}}
201  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 1}}
202}
203
204void compare_different_symbol_minus_left_int_less_or_equal() {
205  int x = f(), y = f();
206  clang_analyzer_denote(x, "$x");
207  clang_analyzer_denote(y, "$y");
208  x -= 1;
209  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 1}}
210}
211
212void compare_different_symbol_plus_right_int_less_or_equal() {
213  int x = f(), y = f();
214  clang_analyzer_denote(x, "$x");
215  clang_analyzer_denote(y, "$y");
216  y += 2;
217  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 2}}
218}
219
220void compare_different_symbol_minus_right_int_less_or_equal() {
221  int x = f(), y = f();
222  clang_analyzer_denote(x, "$x");
223  clang_analyzer_denote(y, "$y");
224  y -= 2;
225  clang_analyzer_express(y); // expected-warning {{$y - 2}}
226  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 2}}
227}
228
229void compare_different_symbol_plus_left_plus_right_int_less_or_equal() {
230  int x = f(), y = f();
231  clang_analyzer_denote(x, "$x");
232  clang_analyzer_denote(y, "$y");
233  x += 2;
234  y += 1;
235  clang_analyzer_express(x); // expected-warning {{$x + 2}}
236  clang_analyzer_express(y); // expected-warning {{$y + 1}}
237  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 1}}
238}
239
240void compare_different_symbol_plus_left_minus_right_int_less_or_equal() {
241  int x = f(), y = f();
242  clang_analyzer_denote(x, "$x");
243  clang_analyzer_denote(y, "$y");
244  x += 2;
245  y -= 1;
246  clang_analyzer_express(x); // expected-warning {{$x + 2}}
247  clang_analyzer_express(y); // expected-warning {{$y - 1}}
248  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 3}}
249}
250
251void compare_different_symbol_minus_left_plus_right_int_less_or_equal() {
252  int x = f(), y = f();
253  clang_analyzer_denote(x, "$x");
254  clang_analyzer_denote(y, "$y");
255  x -= 2;
256  y += 1;
257  clang_analyzer_express(x); // expected-warning {{$x - 2}}
258  clang_analyzer_express(y); // expected-warning {{$y + 1}}
259  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 3}}
260}
261
262void compare_different_symbol_minus_left_minus_right_int_less_or_equal() {
263  int x = f(), y = f();
264  clang_analyzer_denote(x, "$x");
265  clang_analyzer_denote(y, "$y");
266  x -= 2;
267  y -= 1;
268  clang_analyzer_express(x); // expected-warning {{$x - 2}}
269  clang_analyzer_express(y); // expected-warning {{$y - 1}}
270  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 1}}
271}
272
273void compare_same_symbol_less_or_equal() {
274  int x = f(), y = x;
275  clang_analyzer_denote(x, "$x");
276  clang_analyzer_express(y); // expected-warning {{$x}}
277  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
278}
279
280void compare_same_symbol_plus_left_int_less_or_equal() {
281  int x = f(), y = x;
282  clang_analyzer_denote(x, "$x");
283  ++x;
284  clang_analyzer_express(x); // expected-warning {{$x + 1}}
285  clang_analyzer_express(y); // expected-warning {{$x}}
286  clang_analyzer_eval(x <= y); // expected-warning {{FALSE}}
287}
288
289void compare_same_symbol_minus_left_int_less_or_equal() {
290  int x = f(), y = x;
291  clang_analyzer_denote(x, "$x");
292  --x;
293  clang_analyzer_express(x); // expected-warning {{$x - 1}}
294  clang_analyzer_express(y); // expected-warning {{$x}}
295  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
296}
297
298void compare_same_symbol_plus_right_int_less_or_equal() {
299  int x = f(), y = x + 1;
300  clang_analyzer_denote(x, "$x");
301  clang_analyzer_express(y); // expected-warning {{$x + 1}}
302  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
303}
304
305void compare_same_symbol_minus_right_int_less_or_equal() {
306  int x = f(), y = x - 1;
307  clang_analyzer_denote(x, "$x");
308  clang_analyzer_express(y); // expected-warning {{$x - 1}}
309  clang_analyzer_eval(x <= y); // expected-warning {{FALSE}}
310}
311
312void compare_same_symbol_plus_left_plus_right_int_less_or_equal() {
313  int x = f(), y = x + 1;
314  clang_analyzer_denote(x, "$x");
315  ++x;
316  clang_analyzer_express(x); // expected-warning {{$x + 1}}
317  clang_analyzer_express(y); // expected-warning {{$x + 1}}
318  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
319}
320
321void compare_same_symbol_plus_left_minus_right_int_less_or_equal() {
322  int x = f(), y = x - 1;
323  clang_analyzer_denote(x, "$x");
324  ++x;
325  clang_analyzer_express(x); // expected-warning {{$x + 1}}
326  clang_analyzer_express(y); // expected-warning {{$x - 1}}
327  clang_analyzer_eval(x <= y); // expected-warning {{FALSE}}
328}
329
330void compare_same_symbol_minus_left_plus_right_int_less_or_equal() {
331  int x = f(), y = x + 1;
332  clang_analyzer_denote(x, "$x");
333  --x;
334  clang_analyzer_express(x); // expected-warning {{$x - 1}}
335  clang_analyzer_express(y); // expected-warning {{$x + 1}}
336  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
337}
338
339void compare_same_symbol_minus_left_minus_right_int_less_or_equal() {
340  int x = f(), y = x - 1;
341  clang_analyzer_denote(x, "$x");
342  --x;
343  clang_analyzer_express(x); // expected-warning {{$x - 1}}
344  clang_analyzer_express(y); // expected-warning {{$x - 1}}
345  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
346}
347
348void compare_different_symbol_less() {
349  int x = f(), y = f();
350  clang_analyzer_denote(x, "$x");
351  clang_analyzer_denote(y, "$y");
352  clang_analyzer_express(y); // expected-warning {{$y}}
353  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 0}}
354}
355
356void compare_different_symbol_plus_left_int_less() {
357  int x = f(), y = f();
358  clang_analyzer_denote(x, "$x");
359  clang_analyzer_denote(y, "$y");
360  x += 1;
361  clang_analyzer_express(x); // expected-warning {{$x + 1}}
362  clang_analyzer_express(y); // expected-warning {{$y}}
363  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 1}}
364}
365
366void compare_different_symbol_minus_left_int_less() {
367  int x = f(), y = f();
368  clang_analyzer_denote(x, "$x");
369  clang_analyzer_denote(y, "$y");
370  x -= 1;
371  clang_analyzer_express(x); // expected-warning {{$x - 1}}
372  clang_analyzer_express(y); // expected-warning {{$y}}
373  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 1}}
374}
375
376void compare_different_symbol_plus_right_int_less() {
377  int x = f(), y = f();
378  clang_analyzer_denote(x, "$x");
379  clang_analyzer_denote(y, "$y");
380  y += 2;
381  clang_analyzer_express(y); // expected-warning {{$y + 2}}
382  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 2}}
383}
384
385void compare_different_symbol_minus_right_int_less() {
386  int x = f(), y = f();
387  clang_analyzer_denote(x, "$x");
388  clang_analyzer_denote(y, "$y");
389  y -= 2;
390  clang_analyzer_express(y); // expected-warning {{$y - 2}}
391  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 2}}
392}
393
394void compare_different_symbol_plus_left_plus_right_int_less() {
395  int x = f(), y = f();
396  clang_analyzer_denote(x, "$x");
397  clang_analyzer_denote(y, "$y");
398  x += 2;
399  y += 1;
400  clang_analyzer_express(x); // expected-warning {{$x + 2}}
401  clang_analyzer_express(y); // expected-warning {{$y + 1}}
402  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 1}}
403}
404
405void compare_different_symbol_plus_left_minus_right_int_less() {
406  int x = f(), y = f();
407  clang_analyzer_denote(x, "$x");
408  clang_analyzer_denote(y, "$y");
409  x += 2;
410  y -= 1;
411  clang_analyzer_express(x); // expected-warning {{$x + 2}}
412  clang_analyzer_express(y); // expected-warning {{$y - 1}}
413  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 3}}
414}
415
416void compare_different_symbol_minus_left_plus_right_int_less() {
417  int x = f(), y = f();
418  clang_analyzer_denote(x, "$x");
419  clang_analyzer_denote(y, "$y");
420  x -= 2;
421  y += 1;
422  clang_analyzer_express(x); // expected-warning {{$x - 2}}
423  clang_analyzer_express(y); // expected-warning {{$y + 1}}
424  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 3}}
425}
426
427void compare_different_symbol_minus_left_minus_right_int_less() {
428  int x = f(), y = f();
429  clang_analyzer_denote(x, "$x");
430  clang_analyzer_denote(y, "$y");
431  x -= 2;
432  y -= 1;
433  clang_analyzer_express(x); // expected-warning {{$x - 2}}
434  clang_analyzer_express(y); // expected-warning {{$y - 1}}
435  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 1}}
436}
437
438void compare_same_symbol_less() {
439  int x = f(), y = x;
440  clang_analyzer_denote(x, "$x");
441  clang_analyzer_express(y); // expected-warning {{$x}}
442  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
443}
444
445void compare_same_symbol_plus_left_int_less() {
446  int x = f(), y = x;
447  clang_analyzer_denote(x, "$x");
448  ++x;
449  clang_analyzer_express(x); // expected-warning {{$x + 1}}
450  clang_analyzer_express(y); // expected-warning {{$x}}
451  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
452}
453
454void compare_same_symbol_minus_left_int_less() {
455  int x = f(), y = x;
456  clang_analyzer_denote(x, "$x");
457  --x;
458  clang_analyzer_express(x); // expected-warning {{$x - 1}}
459  clang_analyzer_express(y); // expected-warning {{$x}}
460  clang_analyzer_eval(x < y); // expected-warning {{TRUE}}
461}
462
463void compare_same_symbol_plus_right_int_less() {
464  int x = f(), y = x + 1;
465  clang_analyzer_denote(x, "$x");
466  clang_analyzer_express(y); // expected-warning {{$x + 1}}
467  clang_analyzer_eval(x < y); // expected-warning {{TRUE}}
468}
469
470void compare_same_symbol_minus_right_int_less() {
471  int x = f(), y = x - 1;
472  clang_analyzer_denote(x, "$x");
473  clang_analyzer_express(y); // expected-warning {{$x - 1}}
474  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
475}
476
477void compare_same_symbol_plus_left_plus_right_int_less() {
478  int x = f(), y = x + 1;
479  clang_analyzer_denote(x, "$x");
480  ++x;
481  clang_analyzer_express(x); // expected-warning {{$x + 1}}
482  clang_analyzer_express(y); // expected-warning {{$x + 1}}
483  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
484}
485
486void compare_same_symbol_plus_left_minus_right_int_less() {
487  int x = f(), y = x - 1;
488  clang_analyzer_denote(x, "$x");
489  ++x;
490  clang_analyzer_express(x); // expected-warning {{$x + 1}}
491  clang_analyzer_express(y); // expected-warning {{$x - 1}}
492  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
493}
494
495void compare_same_symbol_minus_left_plus_right_int_less() {
496  int x = f(), y = x + 1;
497  clang_analyzer_denote(x, "$x");
498  --x;
499  clang_analyzer_express(x); // expected-warning {{$x - 1}}
500  clang_analyzer_express(y); // expected-warning {{$x + 1}}
501  clang_analyzer_eval(x < y); // expected-warning {{TRUE}}
502}
503
504void compare_same_symbol_minus_left_minus_right_int_less() {
505  int x = f(), y = x - 1;
506  clang_analyzer_denote(x, "$x");
507  --x;
508  clang_analyzer_express(x); // expected-warning {{$x - 1}}
509  clang_analyzer_express(y); // expected-warning {{$x - 1}}
510  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
511}
512
513void compare_different_symbol_equal_unsigned() {
514  unsigned x = f(), y = f();
515  clang_analyzer_denote(x, "$x");
516  clang_analyzer_denote(y, "$y");
517  clang_analyzer_express(y); // expected-warning {{$y}}
518  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 0}}
519}
520
521void compare_different_symbol_plus_left_int_equal_unsigned() {
522  unsigned x = f() + 1, y = f();
523  clang_analyzer_denote(x - 1, "$x");
524  clang_analyzer_denote(y, "$y");
525  clang_analyzer_express(x); // expected-warning {{$x + 1}}
526  clang_analyzer_express(y); // expected-warning {{$y}}
527  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 1}}
528}
529
530void compare_different_symbol_minus_left_int_equal_unsigned() {
531  unsigned x = f() - 1, y = f();
532  clang_analyzer_denote(x + 1, "$x");
533  clang_analyzer_denote(y, "$y");
534  clang_analyzer_express(x); // expected-warning {{$x - 1}}
535  clang_analyzer_express(y); // expected-warning {{$y}}
536  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 1}}
537}
538
539void compare_different_symbol_plus_right_int_equal_unsigned() {
540  unsigned x = f(), y = f() + 2;
541  clang_analyzer_denote(x, "$x");
542  clang_analyzer_denote(y - 2, "$y");
543  clang_analyzer_express(y); // expected-warning {{$y + 2}}
544  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 2}}
545}
546
547void compare_different_symbol_minus_right_int_equal_unsigned() {
548  unsigned x = f(), y = f() - 2;
549  clang_analyzer_denote(x, "$x");
550  clang_analyzer_denote(y + 2, "$y");
551  clang_analyzer_express(y); // expected-warning {{$y - 2}}
552  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 2}}
553}
554
555void compare_different_symbol_plus_left_plus_right_int_equal_unsigned() {
556  unsigned x = f() + 2, y = f() + 1;
557  clang_analyzer_denote(x - 2, "$x");
558  clang_analyzer_denote(y - 1, "$y");
559  clang_analyzer_express(x); // expected-warning {{$x + 2}}
560  clang_analyzer_express(y); // expected-warning {{$y + 1}}
561  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 1}}
562}
563
564void compare_different_symbol_plus_left_minus_right_int_equal_unsigned() {
565  unsigned x = f() + 2, y = f() - 1;
566  clang_analyzer_denote(x - 2, "$x");
567  clang_analyzer_denote(y + 1, "$y");
568  clang_analyzer_express(x); // expected-warning {{$x + 2}}
569  clang_analyzer_express(y); // expected-warning {{$y - 1}}
570  clang_analyzer_express(x == y); // expected-warning {{$y - $x == 3}}
571}
572
573void compare_different_symbol_minus_left_plus_right_int_equal_unsigned() {
574  unsigned x = f() - 2, y = f() + 1;
575  clang_analyzer_denote(x + 2, "$x");
576  clang_analyzer_denote(y - 1, "$y");
577  clang_analyzer_express(x); // expected-warning {{$x - 2}}
578  clang_analyzer_express(y); // expected-warning {{$y + 1}}
579  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 3}}
580}
581
582void compare_different_symbol_minus_left_minus_right_int_equal_unsigned() {
583  unsigned x = f() - 2, y = f() - 1;
584  clang_analyzer_denote(x + 2, "$x");
585  clang_analyzer_denote(y + 1, "$y");
586  clang_analyzer_express(x); // expected-warning {{$x - 2}}
587  clang_analyzer_express(y); // expected-warning {{$y - 1}}
588  clang_analyzer_express(x == y); // expected-warning {{$x - $y == 1}}
589}
590
591void compare_same_symbol_equal_unsigned() {
592  unsigned x = f(), y = x;
593  clang_analyzer_denote(x, "$x");
594  clang_analyzer_express(y); // expected-warning {{$x}}
595  clang_analyzer_eval(x == y); // expected-warning {{TRUE}}
596}
597
598void compare_same_symbol_plus_left_int_equal_unsigned() {
599  unsigned x = f(), y = x;
600  clang_analyzer_denote(x, "$x");
601  ++x;
602  clang_analyzer_express(x); // expected-warning {{$x + 1}}
603  clang_analyzer_express(y); // expected-warning {{$x}}
604  clang_analyzer_express(x == y); // expected-warning {{$x + 1U == $x}}
605}
606
607void compare_same_symbol_minus_left_int_equal_unsigned() {
608  unsigned x = f(), y = x;
609  clang_analyzer_denote(x, "$x");
610  --x;
611  clang_analyzer_express(x); // expected-warning {{$x - 1}}
612  clang_analyzer_express(y); // expected-warning {{$x}}
613  clang_analyzer_express(x == y); // expected-warning {{$x - 1U == $x}}
614}
615
616void compare_same_symbol_plus_right_int_equal_unsigned() {
617  unsigned x = f(), y = x + 1;
618  clang_analyzer_denote(x, "$x");
619  clang_analyzer_express(y); // expected-warning {{$x + 1}}
620  clang_analyzer_express(x == y); // expected-warning {{$x == $x + 1U}}
621}
622
623void compare_same_symbol_minus_right_int_equal_unsigned() {
624  unsigned x = f(), y = x - 1;
625  clang_analyzer_denote(x, "$x");
626  clang_analyzer_express(y); // expected-warning {{$x - 1}}
627  clang_analyzer_express(x == y); // expected-warning {{$x == $x - 1U}}
628}
629
630void compare_same_symbol_plus_left_plus_right_int_equal_unsigned() {
631  unsigned x = f(), y = x + 1;
632  clang_analyzer_denote(x, "$x");
633  ++x;
634  clang_analyzer_express(x); // expected-warning {{$x + 1}}
635  clang_analyzer_express(y); // expected-warning {{$x + 1}}
636  clang_analyzer_eval(x == y); // expected-warning {{TRUE}}
637}
638
639void compare_same_symbol_plus_left_minus_right_int_equal_unsigned() {
640  unsigned x = f(), y = x - 1;
641  clang_analyzer_denote(x, "$x");
642  ++x;
643  clang_analyzer_express(x); // expected-warning {{$x + 1}}
644  clang_analyzer_express(y); // expected-warning {{$x - 1}}
645  clang_analyzer_express(x == y); // expected-warning {{$x + 1U == $x - 1U}}
646}
647
648void compare_same_symbol_minus_left_plus_right_int_equal_unsigned() {
649  unsigned x = f(), y = x + 1;
650  clang_analyzer_denote(x, "$x");
651  --x;
652  clang_analyzer_express(x); // expected-warning {{$x - 1}}
653  clang_analyzer_express(y); // expected-warning {{$x + 1}}
654  clang_analyzer_express(x == y); // expected-warning {{$x - 1U == $x + 1U}}
655}
656
657void compare_same_symbol_minus_left_minus_right_int_equal_unsigned() {
658  unsigned x = f(), y = x - 1;
659  clang_analyzer_denote(x, "$x");
660  --x;
661  clang_analyzer_express(x); // expected-warning {{$x - 1}}
662  clang_analyzer_express(y); // expected-warning {{$x - 1}}
663  clang_analyzer_eval(x == y); // expected-warning {{TRUE}}
664}
665
666void compare_different_symbol_less_or_equal_unsigned() {
667  unsigned x = f(), y = f();
668  clang_analyzer_denote(x, "$x");
669  clang_analyzer_denote(y, "$y");
670  clang_analyzer_express(y); // expected-warning {{$y}}
671  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 0}}
672}
673
674void compare_different_symbol_plus_left_int_less_or_equal_unsigned() {
675  unsigned x = f() + 1, y = f();
676  clang_analyzer_denote(x - 1, "$x");
677  clang_analyzer_denote(y, "$y");
678  clang_analyzer_express(x); // expected-warning {{$x + 1}}
679  clang_analyzer_express(y); // expected-warning {{$y}}
680  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 1}}
681}
682
683void compare_different_symbol_minus_left_int_less_or_equal_unsigned() {
684  unsigned x = f() - 1, y = f();
685  clang_analyzer_denote(x + 1, "$x");
686  clang_analyzer_denote(y, "$y");
687  clang_analyzer_express(x); // expected-warning {{$x - 1}}
688  clang_analyzer_express(y); // expected-warning {{$y}}
689  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 1}}
690}
691
692void compare_different_symbol_plus_right_int_less_or_equal_unsigned() {
693  unsigned x = f(), y = f() + 2;
694  clang_analyzer_denote(x, "$x");
695  clang_analyzer_denote(y - 2, "$y");
696  clang_analyzer_express(y); // expected-warning {{$y + 2}}
697  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 2}}
698}
699
700void compare_different_symbol_minus_right_int_less_or_equal_unsigned() {
701  unsigned x = f(), y = f() - 2;
702  clang_analyzer_denote(x, "$x");
703  clang_analyzer_denote(y + 2, "$y");
704  clang_analyzer_express(y); // expected-warning {{$y - 2}}
705  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 2}}
706}
707
708void compare_different_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
709  unsigned x = f() + 2, y = f() + 1;
710  clang_analyzer_denote(x - 2, "$x");
711  clang_analyzer_denote(y - 1, "$y");
712  clang_analyzer_express(x); // expected-warning {{$x + 2}}
713  clang_analyzer_express(y); // expected-warning {{$y + 1}}
714  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 1}}
715}
716
717void compare_different_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
718  unsigned x = f() + 2, y = f() - 1;
719  clang_analyzer_denote(x - 2, "$x");
720  clang_analyzer_denote(y + 1, "$y");
721  clang_analyzer_express(x); // expected-warning {{$x + 2}}
722  clang_analyzer_express(y); // expected-warning {{$y - 1}}
723  clang_analyzer_express(x <= y); // expected-warning {{$y - $x >= 3}}
724}
725
726void compare_different_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
727  unsigned x = f() - 2, y = f() + 1;
728  clang_analyzer_denote(x + 2, "$x");
729  clang_analyzer_denote(y - 1, "$y");
730  clang_analyzer_express(x); // expected-warning {{$x - 2}}
731  clang_analyzer_express(y); // expected-warning {{$y + 1}}
732  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 3}}
733}
734
735void compare_different_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
736  unsigned x = f() - 2, y = f() - 1;
737  clang_analyzer_denote(x + 2, "$x");
738  clang_analyzer_denote(y + 1, "$y");
739  clang_analyzer_express(x); // expected-warning {{$x - 2}}
740  clang_analyzer_express(y); // expected-warning {{$y - 1}}
741  clang_analyzer_express(x <= y); // expected-warning {{$x - $y <= 1}}
742}
743
744void compare_same_symbol_less_or_equal_unsigned() {
745  unsigned x = f(), y = x;
746  clang_analyzer_denote(x, "$x");
747  clang_analyzer_express(y); // expected-warning {{$x}}
748  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
749}
750
751void compare_same_symbol_plus_left_int_less_or_equal_unsigned() {
752  unsigned x = f(), y = x;
753  clang_analyzer_denote(x, "$x");
754  ++x;
755  clang_analyzer_express(x); // expected-warning {{$x + 1}}
756  clang_analyzer_express(y); // expected-warning {{$x}}
757  clang_analyzer_express(x <= y); // expected-warning {{$x + 1U <= $x}}
758}
759
760void compare_same_symbol_minus_left_int_less_or_equal_unsigned() {
761  unsigned x = f(), y = x;
762  clang_analyzer_denote(x, "$x");
763  --x;
764  clang_analyzer_express(x); // expected-warning {{$x - 1}}
765  clang_analyzer_express(y); // expected-warning {{$x}}
766  clang_analyzer_express(x <= y); // expected-warning {{$x - 1U <= $x}}
767}
768
769void compare_same_symbol_plus_right_int_less_or_equal_unsigned() {
770  unsigned x = f(), y = x + 1;
771  clang_analyzer_denote(x, "$x");
772  clang_analyzer_express(y); // expected-warning {{$x + 1}}
773  clang_analyzer_express(x <= y); // expected-warning {{$x <= $x + 1U}}
774}
775
776void compare_same_symbol_minus_right_int_less_or_equal_unsigned() {
777  unsigned x = f(), y = x - 1;
778  clang_analyzer_denote(x, "$x");
779  clang_analyzer_express(y); // expected-warning {{$x - 1}}
780  clang_analyzer_express(x <= y); // expected-warning {{$x <= $x - 1U}}
781}
782
783void compare_same_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
784  unsigned x = f(), y = x + 1;
785  clang_analyzer_denote(x, "$x");
786  ++x;
787  clang_analyzer_express(x); // expected-warning {{$x + 1}}
788  clang_analyzer_express(y); // expected-warning {{$x + 1}}
789  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
790}
791
792void compare_same_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
793  unsigned x = f(), y = x - 1;
794  clang_analyzer_denote(x, "$x");
795  ++x;
796  clang_analyzer_express(x); // expected-warning {{$x + 1}}
797  clang_analyzer_express(y); // expected-warning {{$x - 1}}
798  clang_analyzer_express(x <= y); // expected-warning {{$x + 1U <= $x - 1U}}
799}
800
801void compare_same_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
802  unsigned x = f(), y = x + 1;
803  clang_analyzer_denote(x, "$x");
804  --x;
805  clang_analyzer_express(x); // expected-warning {{$x - 1}}
806  clang_analyzer_express(y); // expected-warning {{$x + 1}}
807  clang_analyzer_express(x <= y); // expected-warning {{$x - 1U <= $x + 1U}}
808}
809
810void compare_same_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
811  unsigned x = f(), y = x - 1;
812  clang_analyzer_denote(x, "$x");
813  --x;
814  clang_analyzer_express(x); // expected-warning {{$x - 1}}
815  clang_analyzer_express(y); // expected-warning {{$x - 1}}
816  clang_analyzer_eval(x <= y); // expected-warning {{TRUE}}
817}
818
819void compare_different_symbol_less_unsigned() {
820  unsigned x = f(), y = f();
821  clang_analyzer_denote(x, "$x");
822  clang_analyzer_denote(y, "$y");
823  clang_analyzer_express(y); // expected-warning {{$y}}
824  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 0}}
825}
826
827void compare_different_symbol_plus_left_int_less_unsigned() {
828  unsigned x = f() + 1, y = f();
829  clang_analyzer_denote(x - 1, "$x");
830  clang_analyzer_denote(y, "$y");
831  clang_analyzer_express(x); // expected-warning {{$x + 1}}
832  clang_analyzer_express(y); // expected-warning {{$y}}
833  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 1}}
834}
835
836void compare_different_symbol_minus_left_int_less_unsigned() {
837  unsigned x = f() - 1, y = f();
838  clang_analyzer_denote(x + 1, "$x");
839  clang_analyzer_denote(y, "$y");
840  clang_analyzer_express(x); // expected-warning {{$x - 1}}
841  clang_analyzer_express(y); // expected-warning {{$y}}
842  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 1}}
843}
844
845void compare_different_symbol_plus_right_int_less_unsigned() {
846  unsigned x = f(), y = f() + 2;
847  clang_analyzer_denote(x, "$x");
848  clang_analyzer_denote(y - 2, "$y");
849  clang_analyzer_express(y); // expected-warning {{$y + 2}}
850  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 2}}
851}
852
853void compare_different_symbol_minus_right_int_less_unsigned() {
854  unsigned x = f(), y = f() - 2;
855  clang_analyzer_denote(x, "$x");
856  clang_analyzer_denote(y + 2, "$y");
857  clang_analyzer_express(y); // expected-warning {{$y - 2}}
858  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 2}}
859}
860
861void compare_different_symbol_plus_left_plus_right_int_less_unsigned() {
862  unsigned x = f() + 2, y = f() + 1;
863  clang_analyzer_denote(x - 2, "$x");
864  clang_analyzer_denote(y - 1, "$y");
865  clang_analyzer_express(x); // expected-warning {{$x + 2}}
866  clang_analyzer_express(y); // expected-warning {{$y + 1}}
867  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 1}}
868}
869
870void compare_different_symbol_plus_left_minus_right_int_less_unsigned() {
871  unsigned x = f() + 2, y = f() - 1;
872  clang_analyzer_denote(x - 2, "$x");
873  clang_analyzer_denote(y + 1, "$y");
874  clang_analyzer_express(x); // expected-warning {{$x + 2}}
875  clang_analyzer_express(y); // expected-warning {{$y - 1}}
876  clang_analyzer_express(x < y); // expected-warning {{$y - $x > 3}}
877}
878
879void compare_different_symbol_minus_left_plus_right_int_less_unsigned() {
880  unsigned x = f() - 2, y = f() + 1;
881  clang_analyzer_denote(x + 2, "$x");
882  clang_analyzer_denote(y - 1, "$y");
883  clang_analyzer_express(x); // expected-warning {{$x - 2}}
884  clang_analyzer_express(y); // expected-warning {{$y + 1}}
885  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 3}}
886}
887
888void compare_different_symbol_minus_left_minus_right_int_less_unsigned() {
889  unsigned x = f() - 2, y = f() - 1;
890  clang_analyzer_denote(x + 2, "$x");
891  clang_analyzer_denote(y + 1, "$y");
892  clang_analyzer_express(x); // expected-warning {{$x - 2}}
893  clang_analyzer_express(y); // expected-warning {{$y - 1}}
894  clang_analyzer_express(x < y); // expected-warning {{$x - $y < 1}}
895}
896
897void compare_same_symbol_less_unsigned() {
898  unsigned x = f(), y = x;
899  clang_analyzer_denote(x, "$x");
900  clang_analyzer_express(y); // expected-warning {{$x}}
901  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
902}
903
904void compare_same_symbol_plus_left_int_less_unsigned() {
905  unsigned x = f(), y = x;
906  clang_analyzer_denote(x, "$x");
907  ++x;
908  clang_analyzer_express(x); // expected-warning {{$x + 1}}
909  clang_analyzer_express(y); // expected-warning {{$x}}
910  clang_analyzer_express(x < y); // expected-warning {{$x + 1U < $x}}
911}
912
913void compare_same_symbol_minus_left_int_less_unsigned() {
914  unsigned x = f(), y = x;
915  clang_analyzer_denote(x, "$x");
916  --x;
917  clang_analyzer_express(x); // expected-warning {{$x - 1}}
918  clang_analyzer_express(y); // expected-warning {{$x}}
919  clang_analyzer_express(x < y); // expected-warning {{$x - 1U < $x}}
920}
921
922void compare_same_symbol_plus_right_int_less_unsigned() {
923  unsigned x = f(), y = x + 1;
924  clang_analyzer_denote(x, "$x");
925  clang_analyzer_express(y); // expected-warning {{$x + 1}}
926  clang_analyzer_express(x < y); // expected-warning {{$x < $x + 1U}}
927}
928
929void compare_same_symbol_minus_right_int_less_unsigned() {
930  unsigned x = f(), y = x - 1;
931  clang_analyzer_denote(x, "$x");
932  clang_analyzer_express(y); // expected-warning {{$x - 1}}
933  clang_analyzer_express(x < y); // expected-warning {{$x < $x - 1U}}
934}
935
936void compare_same_symbol_plus_left_plus_right_int_less_unsigned() {
937  unsigned x = f(), y = x + 1;
938  clang_analyzer_denote(x, "$x");
939  ++x;
940  clang_analyzer_express(x); // expected-warning {{$x + 1}}
941  clang_analyzer_express(y); // expected-warning {{$x + 1}}
942  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
943}
944
945void compare_same_symbol_plus_left_minus_right_int_less_unsigned() {
946  unsigned x = f(), y = x - 1;
947  clang_analyzer_denote(x, "$x");
948  ++x;
949  clang_analyzer_express(x); // expected-warning {{$x + 1}}
950  clang_analyzer_express(y); // expected-warning {{$x - 1}}
951  clang_analyzer_express(x < y); // expected-warning {{$x + 1U < $x - 1U}}
952}
953
954void compare_same_symbol_minus_left_plus_right_int_less_unsigned() {
955  unsigned x = f(), y = x + 1;
956  clang_analyzer_denote(x, "$x");
957  --x;
958  clang_analyzer_express(x); // expected-warning {{$x - 1}}
959  clang_analyzer_express(y); // expected-warning {{$x + 1}}
960  clang_analyzer_express(x < y); // expected-warning {{$x - 1U < $x + 1U}}
961}
962
963void compare_same_symbol_minus_left_minus_right_int_less_unsigned() {
964  unsigned x = f(), y = x - 1;
965  clang_analyzer_denote(x, "$x");
966  --x;
967  clang_analyzer_express(x); // expected-warning {{$x - 1}}
968  clang_analyzer_express(y); // expected-warning {{$x - 1}}
969  clang_analyzer_eval(x < y); // expected-warning {{FALSE}}
970}
971
972void overflow(signed char n, signed char m) {
973  if (n + 0 > m + 0) {
974    clang_analyzer_eval(n - 126 == m + 3); // expected-warning {{UNKNOWN}}
975  }
976}
977
978int mixed_integer_types(int x, int y) {
979  short a = x - 1U;
980  return a - y;
981}
982
983unsigned gu();
984unsigned fu() {
985  unsigned x = gu();
986  // Assert that no overflows occur in this test file.
987  // Assuming that concrete integers are also within that range.
988  assert(x <= ((unsigned)UINT_MAX / 4));
989  return x;
990}
991
992void unsigned_concrete_int_no_crash() {
993  unsigned x = fu() + 1U, y = fu() + 1U;
994  clang_analyzer_denote(x - 1U, "$x");
995  clang_analyzer_denote(y - 1U, "$y");
996  clang_analyzer_express(y); // expected-warning {{$y}}
997  clang_analyzer_express(x == y); // expected-warning {{$x + 1U == $y + 1U}}
998}
999
CodeThinker, Enjoy your reading code