|  | // RUN: %clang_analyze_cc1 %s \ | 
|  | // RUN:   -analyzer-checker=core \ | 
|  | // RUN:   -analyzer-checker=debug.ExprInspection \ | 
|  | // RUN:   -analyzer-config eagerly-assume=false \ | 
|  | // RUN:   -verify | 
|  |  | 
|  | // Here we test whether the SValBuilder is capable to simplify existing | 
|  | // compound SVals (where there are at leaset 3 symbols in the tree) based on | 
|  | // newly added constraints. | 
|  |  | 
|  | void clang_analyzer_eval(bool); | 
|  | void clang_analyzer_warnIfReached(); | 
|  |  | 
|  | void test_left_tree_constrained(int x, int y, int z) { | 
|  | if (x + y + z != 0) | 
|  | return; | 
|  | if (x + y != 0) | 
|  | return; | 
|  | clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}} | 
|  | clang_analyzer_eval(x + y == 0);     // expected-warning{{TRUE}} | 
|  | clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}} | 
|  | x = y = z = 1; | 
|  | return; | 
|  | } | 
|  |  | 
|  | void test_right_tree_constrained(int x, int y, int z) { | 
|  | if (x + y * z != 0) | 
|  | return; | 
|  | if (y * z != 0) | 
|  | return; | 
|  | clang_analyzer_eval(x + y * z == 0); // expected-warning{{TRUE}} | 
|  | clang_analyzer_eval(y * z == 0);     // expected-warning{{TRUE}} | 
|  | clang_analyzer_eval(x == 0);         // expected-warning{{TRUE}} | 
|  | return; | 
|  | } | 
|  |  | 
|  | void test_left_tree_constrained_minus(int x, int y, int z) { | 
|  | if (x - y - z != 0) | 
|  | return; | 
|  | if (x - y != 0) | 
|  | return; | 
|  | clang_analyzer_eval(x - y - z == 0); // expected-warning{{TRUE}} | 
|  | clang_analyzer_eval(x - y == 0);     // expected-warning{{TRUE}} | 
|  | clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}} | 
|  | x = y = z = 1; | 
|  | return; | 
|  | } | 
|  |  | 
|  | void test_SymInt_constrained(int x, int y, int z) { | 
|  | if (x * y * z != 4) | 
|  | return; | 
|  | if (z != 2) | 
|  | return; | 
|  | if (x * y == 3) { | 
|  | clang_analyzer_warnIfReached();     // no-warning | 
|  | return; | 
|  | } | 
|  | (void)(x * y * z); | 
|  | } | 
|  |  | 
|  | void test_SValBuilder_simplifies_IntSym(int x, int y, int z) { | 
|  | // Most IntSym BinOps are transformed to SymInt in SimpleSValBuilder. | 
|  | // Division is one exception. | 
|  | x = 77 / (y + z); | 
|  | if (y + z != 1) | 
|  | return; | 
|  | clang_analyzer_eval(x == 77);         // expected-warning{{TRUE}} | 
|  | (void)(x * y * z); | 
|  | } | 
|  |  | 
|  | void recurring_symbol(int b) { | 
|  | if (b * b != b) | 
|  | if ((b * b) * b * b != (b * b) * b) | 
|  | if (b * b == 1)                   // no-crash (assert should not fire) | 
|  | clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} | 
|  | } |