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
test_contradiction(int a,int b,int c,int d,int x)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
test_true_range_contradiction(int a,unsigned b)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