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 }
56