clang/test/Analysis/svalbuilder-rearrange-comparisons.cpp

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