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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
// RUN: %clang_analyze_cc1 %s \
// RUN: -analyzer-checker=core \
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -verify
void clang_analyzer_warnIfReached();
void clang_analyzer_eval(int);
void rem_constant_rhs_ne_zero(int x, int y) {
if (x % 3 == 0) // x % 3 != 0 -> x != 0
return;
if (x * y != 0) // x * y == 0
return;
if (y != 1) // y == 1 -> x == 0
return;
clang_analyzer_warnIfReached(); // no-warning
(void)x; // keep the constraints alive.
}
void rem_symbolic_rhs_ne_zero(int x, int y, int z) {
if (x % z == 0) // x % z != 0 -> x != 0
return;
if (x * y != 0) // x * y == 0
return;
if (y != 1) // y == 1 -> x == 0
return;
clang_analyzer_warnIfReached(); // no-warning
(void)x; // keep the constraints alive.
}
void rem_symbolic_rhs_ne_zero_nested(int w, int x, int y, int z) {
if (w % x % z == 0) // w % x % z != 0 -> w % x != 0
return;
if (w % x * y != 0) // w % x * y == 0
return;
if (y != 1) // y == 1 -> w % x == 0
return;
clang_analyzer_warnIfReached(); // no-warning
(void)(w * x); // keep the constraints alive.
}
void rem_constant_rhs_ne_zero_early_contradiction(int x, int y) {
if ((x + y) != 0) // (x + y) == 0
return;
if ((x + y) % 3 == 0) // (x + y) % 3 != 0 -> (x + y) != 0 -> contradiction
return;
clang_analyzer_warnIfReached(); // no-warning
(void)x; // keep the constraints alive.
}
void rem_symbolic_rhs_ne_zero_early_contradiction(int x, int y, int z) {
if ((x + y) != 0) // (x + y) == 0
return;
if ((x + y) % z == 0) // (x + y) % z != 0 -> (x + y) != 0 -> contradiction
return;
clang_analyzer_warnIfReached(); // no-warning
(void)x; // keep the constraints alive.
}
void internal_unsigned_signed_mismatch(unsigned a) {
int d = a;
// Implicit casts are not handled, thus the analyzer models `d % 2` as
// `(reg_$0<unsigned int a>) % 2`
// However, this should not result in internal signedness mismatch error when
// we assign new constraints below.
if (d % 2 != 0)
return;
}
void remainder_with_adjustment(int x) {
if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
return;
clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}}
clang_analyzer_eval(x != -1); // expected-warning{{TRUE}}
(void)x; // keep the constraints alive.
}
void remainder_with_adjustment_of_composit_lhs(int x, int y) {
if ((x + y + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
return;
clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}}
clang_analyzer_eval(x + y != -1); // expected-warning{{TRUE}}
(void)(x * y); // keep the constraints alive.
}
|
