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