1 // RUN: %clang_analyze_cc1 %s \
2 // RUN: -analyzer-checker=core \
3 // RUN: -analyzer-checker=debug.ExprInspection \
4 // RUN: -analyzer-config eagerly-assume=false \
5 // RUN: -verify
6
7 void clang_analyzer_warnIfReached(void);
8 void clang_analyzer_eval(_Bool);
9
test_simplification_adjustment_concrete_int(int b,int c)10 void test_simplification_adjustment_concrete_int(int b, int c) {
11 if (b < 0 || b > 1) // b: [0,1]
12 return;
13 if (c < -1 || c > 1) // c: [-1,1]
14 return;
15 if (c + b != 0) // c + b == 0
16 return;
17 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
18 if (b != 1) // b == 1 --> c + 1 == 0 --> c == -1
19 return;
20 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
21 clang_analyzer_eval(c == -1); // expected-warning{{TRUE}}
22
23 // Keep the symbols and the constraints! alive.
24 (void)(b * c);
25 return;
26 }
27
test_simplification_adjustment_range(int b,int c)28 void test_simplification_adjustment_range(int b, int c) {
29 if (b < 0 || b > 1) // b: [0,1]
30 return;
31 if (c < -1 || c > 1) // c: [-1,1]
32 return;
33 if (c + b < -1 || c + b > 0) // c + b: [-1,0]
34 return;
35 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
36 if (b != 1) // b == 1 --> c + 1: [-1,0] --> c: [-2,-1]
37 return;
38 // c: [-2,-1] is intersected with the
39 // already associated range which is [-1,1],
40 // thus we get c: [-1,-1]
41 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
42 clang_analyzer_eval(c == -1); // expected-warning{{TRUE}}
43
44 // Keep the symbols and the constraints! alive.
45 (void)(b * c);
46 return;
47 }
48
test_simplification_adjustment_to_infeasible_concrete_int(int b,int c)49 void test_simplification_adjustment_to_infeasible_concrete_int(int b, int c) {
50 if (b < 0 || b > 1) // b: [0,1]
51 return;
52 if (c < 0 || c > 1) // c: [0,1]
53 return;
54 if (c + b != 0) // c + b == 0
55 return;
56 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
57 if (b != 1) { // b == 1 --> c + 1 == 0 --> c == -1 contradiction
58 clang_analyzer_eval(b == 0); // expected-warning{{TRUE}}
59 clang_analyzer_eval(c == 0); // expected-warning{{TRUE}}
60 // Keep the symbols and the constraints! alive.
61 (void)(b * c);
62 return;
63 }
64 clang_analyzer_warnIfReached(); // no warning
65
66 // Keep the symbols and the constraints! alive.
67 (void)(b * c);
68 return;
69 }
70
test_simplification_adjustment_to_infeassible_range(int b,int c)71 void test_simplification_adjustment_to_infeassible_range(int b, int c) {
72 if (b < 0 || b > 1) // b: [0,1]
73 return;
74 if (c < 0 || c > 1) // c: [0,1]
75 return;
76 if (c + b < -1 || c + b > 0) // c + b: [-1,0]
77 return;
78 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
79 if (b != 1) // b == 1 --> c + 1: [-1,0] --> c: [-2,-1] contradiction
80 return;
81 clang_analyzer_warnIfReached(); // no warning
82
83 // Keep the symbols and the constraints! alive.
84 (void)(b * c);
85 return;
86 }
87
test_simplification_adjusment_no_infinite_loop(int a,int b,int c)88 void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) {
89 if (a == b) // a != b
90 return;
91 if (c != 0) // c == 0
92 return;
93
94 if (b != 0) // b == 0
95 return;
96 // The above simplification of `b == 0` could result in an infinite loop
97 // unless we detect that the State is unchanged.
98 // The loop:
99 // 1) Simplification of the trivial equivalence class
100 // "symbol": "(reg_$0<int a>) == (reg_$1<int b>)", "range": "{ [0, 0] }"
101 // results in
102 // "symbol": "(reg_$0<int a>) == 0", "range": "{ [0, 0] }" }
103 // which in turn creates a non-trivial equivalence class
104 // [ "(reg_$0<int a>) == (reg_$1<int b>)", "(reg_$0<int a>) == 0" ]
105 // 2) We call assumeSymInclusiveRange("(reg_$0<int a>) == 0")
106 // and that calls **simplify** on the associated non-trivial equivalence
107 // class. During the simplification the State does not change, we reached
108 // the fixpoint.
109
110 (void)(a * b * c);
111 }
112