112 lines · c
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: -verify6 7void clang_analyzer_warnIfReached(void);8void clang_analyzer_eval(_Bool);9 10void 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 == 016 return;17 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}18 if (b != 1) // b == 1 --> c + 1 == 0 --> c == -119 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 28void 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 the39 // 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 49void 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 == 055 return;56 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}57 if (b != 1) { // b == 1 --> c + 1 == 0 --> c == -1 contradiction58 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 warning65 66 // Keep the symbols and the constraints! alive.67 (void)(b * c);68 return;69}70 71void 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] contradiction80 return;81 clang_analyzer_warnIfReached(); // no warning82 83 // Keep the symbols and the constraints! alive.84 (void)(b * c);85 return;86}87 88void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) {89 if (a == b) // a != b90 return;91 if (c != 0) // c == 092 return;93 94 if (b != 0) // b == 095 return;96 // The above simplification of `b == 0` could result in an infinite loop97 // unless we detect that the State is unchanged.98 // The loop:99 // 1) Simplification of the trivial equivalence class100 // "symbol": "(reg_$0<int a>) == (reg_$1<int b>)", "range": "{ [0, 0] }"101 // results in102 // "symbol": "(reg_$0<int a>) == 0", "range": "{ [0, 0] }" }103 // which in turn creates a non-trivial equivalence class104 // [ "(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 equivalence107 // class. During the simplification the State does not change, we reached108 // the fixpoint.109 110 (void)(a * b * c);111}112