clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp

   1 // RUN: %clang_analyze_cc1 %s \
   2 // RUN:   -analyzer-checker=core \
   3 // RUN:   -analyzer-checker=debug.ExprInspection \
   4 // RUN:   -verify
   5
   6 // In this test we check whether the solver's symbol simplification mechanism
   7 // is capable of reaching a fixpoint.
   8
   9 void clang_analyzer_warnIfReached();
  10
  11 void test_contradiction(int a, int b, int c, int d, int x) {
  12   if (a + b + c != d)
  13     return;
  14   if (a == d)
  15     return;
  16   if (b + c != 0)
  17     return;
  18   clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  19
  20   // Bring in the contradiction.
  21   if (b != 0)
  22     return;
  23
  24   // After the simplification of `b == 0` we have:
  25   //   b == 0
  26   //   a + c == d
  27   //   a != d
  28   //   c == 0
  29   // Doing another iteration we reach the fixpoint (with a contradiction):
  30   //   b == 0
  31   //   a == d
  32   //   a != d
  33   //   c == 0
  34   clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
  35
  36   // Enabling expensive checks would trigger an assertion failure here without
  37   // the fixpoint iteration.
  38   if (a + c == x)
  39     return;
  40
  41   // Keep the symbols and the constraints! alive.
  42   (void)(a * b * c * d * x);
  43   return;
  44 }
  45
  46 void test_true_range_contradiction(int a, unsigned b) {
  47   if (!(b > a))   // unsigned b > int a
  48     return;
  49   if (a != -1)    // int a == -1
  50     return;       // Starts a simplification of `unsigned b > int a`,
  51                   // that results in `unsigned b > UINT_MAX`,
  52                   // which is always false, so the State is infeasible.
  53   clang_analyzer_warnIfReached(); // no-warning
  54   (void)(a * b);
  55 }