annotate clang/test/Analysis/equality_tracking.c @ 222:81f6424ef0e3 llvm-original

LLVM original branch
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 18 Jul 2021 22:10:01 +0900 (2021-07-18)
parents 79ff65ed7e25
children 5f17cb93ff66
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
221
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 // RUN: %clang_analyze_cc1 -verify %s \
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 // RUN: -analyzer-checker=core,debug.ExprInspection \
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 // RUN: -analyzer-config eagerly-assume=false
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 #define NULL (void *)0
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 #define UCHAR_MAX (unsigned char)(~0U)
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 #define CHAR_MAX (char)(UCHAR_MAX & (UCHAR_MAX >> 1))
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 #define CHAR_MIN (char)(UCHAR_MAX & ~(UCHAR_MAX >> 1))
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 void clang_analyzer_eval(int);
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 void clang_analyzer_warnIfReached();
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 int getInt();
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 void zeroImpliesEquality(int a, int b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 clang_analyzer_eval((a - b) == 0); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 if ((a - b) == 0) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 clang_analyzer_eval(b != a); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 clang_analyzer_eval(b == a); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 clang_analyzer_eval(!(a != b)); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 clang_analyzer_eval(!(b == a)); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 clang_analyzer_eval((a - b) == 0); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 clang_analyzer_eval(b == a); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 clang_analyzer_eval(b != a); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 void zeroImpliesReversedEqual(int a, int b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 clang_analyzer_eval((b - a) == 0); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 if ((b - a) == 0) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 clang_analyzer_eval(b != a); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 clang_analyzer_eval(b == a); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 clang_analyzer_eval((b - a) == 0); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 clang_analyzer_eval(b == a); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 clang_analyzer_eval(b != a); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 void canonicalEqual(int a, int b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 if (a == b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 clang_analyzer_eval(b == a); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 clang_analyzer_eval(a == b); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 clang_analyzer_eval(b == a); // expected-warning{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 void test(int a, int b, int c, int d) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 if (a == b && c == d) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 if (a == 0 && b == d) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 clang_analyzer_eval(c == 0); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 c = 10;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 if (b == d) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 clang_analyzer_eval(c == 10); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 clang_analyzer_eval(d == 10); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 // expected-warning@-1{{FALSE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 clang_analyzer_eval(b == a); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 clang_analyzer_eval(a == d); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 b = getInt();
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 clang_analyzer_eval(a == d); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 if (a != b && b == c) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 if (c == 42) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 clang_analyzer_eval(b == 42); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 clang_analyzer_eval(a != 42); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 void testIntersection(int a, int b, int c) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 if (a < 42 && b > 15 && c >= 25 && c <= 30) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 if (a != b)
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 clang_analyzer_eval(a > 15); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 clang_analyzer_eval(b < 42); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 clang_analyzer_eval(a <= 30); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 if (c == b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 // For all equal symbols, we should track the minimal common range.
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 //
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 // Also, it should be noted that c is dead at this point, but the
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 // constraint initially associated with c is still around.
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 clang_analyzer_eval(a >= 25 && a <= 30); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 clang_analyzer_eval(b >= 25 && b <= 30); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 void testPromotion(int a, char b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 if (b > 10) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 if (a == b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 // FIXME: support transferring char ranges onto equal int symbols
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 // when char is promoted to int
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 clang_analyzer_eval(a > 10); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 clang_analyzer_eval(a <= CHAR_MAX); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 void testPromotionOnlyTypes(int a, char b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 if (a == b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 // FIXME: support transferring char ranges onto equal int symbols
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 // when char is promoted to int
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 clang_analyzer_eval(a <= CHAR_MAX); // expected-warning{{UNKNOWN}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 void testDowncast(int a, unsigned char b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 if (a <= -10) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 if ((unsigned char)a == b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 // Even though ranges for a and b do not intersect,
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 // ranges for (unsigned char)a and b do.
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 if (a == b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 // FIXME: This case on the other hand is different, it shouldn't be
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 // reachable. However, the corrent symbolic information available
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 // to the solver doesn't allow it to distinguish this expression
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 // from the previous one.
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 void testPointers(int *a, int *b, int *c, int *d) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 if (a == b && c == d) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 if (a == NULL && b == d) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 clang_analyzer_eval(c == NULL); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 if (a != b && b == c) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 if (c == NULL) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 clang_analyzer_eval(a != NULL); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 void testDisequalitiesAfter(int a, int b, int c) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 if (a >= 10 && b <= 42) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 if (a == b && c == 15 && c != a) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 clang_analyzer_eval(b != c); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 clang_analyzer_eval(a != 15); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 clang_analyzer_eval(b != 15); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 clang_analyzer_eval(b >= 10); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 clang_analyzer_eval(a <= 42); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 void testDisequalitiesBefore(int a, int b, int c) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 if (a >= 10 && b <= 42 && c == 15) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 if (a == b && c != a) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 clang_analyzer_eval(b != c); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 clang_analyzer_eval(a != 15); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 clang_analyzer_eval(b != 15); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 clang_analyzer_eval(b >= 10); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 clang_analyzer_eval(a <= 42); // expected-warning{{TRUE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 void avoidInfeasibleConstraintsForClasses(int a, int b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 if (a >= 0 && a <= 10 && b >= 20 && b <= 50) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 if ((b - a) == 0) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176 clang_analyzer_warnIfReached(); // no warning
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 if (a == b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 clang_analyzer_warnIfReached(); // no warning
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181 if (a != b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 } else {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 clang_analyzer_warnIfReached(); // no warning
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 void avoidInfeasibleConstraintforGT(int a, int b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 int c = b - a;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191 if (c <= 0)
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193 // c > 0
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194 // b - a > 0
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 // b > a
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196 if (a != b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200 clang_analyzer_warnIfReached(); // no warning
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
201 // a == b
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
202 if (c < 0)
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
203 ;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206 void avoidInfeasibleConstraintforLT(int a, int b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 int c = b - a;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
208 if (c >= 0)
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
209 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
210 // c < 0
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
211 // b - a < 0
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
212 // b < a
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
213 if (a != b) {
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
214 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
215 return;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
216 }
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217 clang_analyzer_warnIfReached(); // no warning
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
218 // a == b
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
219 if (c < 0)
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
220 ;
79ff65ed7e25 LLVM12 Original
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
221 }