56 lines · cpp
1// RUN: %clang_analyze_cc1 %s \2// RUN: -analyzer-checker=core \3// RUN: -analyzer-checker=debug.ExprInspection \4// RUN: -verify5 6// In this test we check whether the solver's symbol simplification mechanism7// is capable of reaching a fixpoint.8 9void clang_analyzer_warnIfReached();10 11void test_contradiction(int a, int b, int c, int d, int x) {12 if (a + b + c != d)13 return;14 if (a == d)15 return;16 if (b + c != 0)17 return;18 clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}19 20 // Bring in the contradiction.21 if (b != 0)22 return;23 24 // After the simplification of `b == 0` we have:25 // b == 026 // a + c == d27 // a != d28 // c == 029 // Doing another iteration we reach the fixpoint (with a contradiction):30 // b == 031 // a == d32 // a != d33 // c == 034 clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE35 36 // Enabling expensive checks would trigger an assertion failure here without37 // the fixpoint iteration.38 if (a + c == x)39 return;40 41 // Keep the symbols and the constraints! alive.42 (void)(a * b * c * d * x);43 return;44}45 46void test_true_range_contradiction(int a, unsigned b) {47 if (!(b > a)) // unsigned b > int a48 return;49 if (a != -1) // int a == -150 return; // Starts a simplification of `unsigned b > int a`,51 // that results in `unsigned b > UINT_MAX`,52 // which is always false, so the State is infeasible.53 clang_analyzer_warnIfReached(); // no-warning54 (void)(a * b);55}56